diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index 073ad267476c4..1995300c5bcbb 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -351,7 +351,7 @@ you need to pull rustc changes into Miri first, and then re-do the rustc push. If this fails due to authentication problems, it can help to make josh push via ssh instead of https. Add the following to your `.gitconfig`: -```toml +```text [url "git@github.com:"] pushInsteadOf = https://github.com/ ``` diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index 32494141589ac..86f190134d452 100644 --- a/src/tools/miri/README.md +++ b/src/tools/miri/README.md @@ -651,6 +651,11 @@ Violations of [Stacked Borrows] found that are likely bugs (but Stacked Borrows * [Stacked Borrows: An Aliasing Model for Rust](https://plv.mpi-sws.org/rustbelt/stacked-borrows/) * [Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3](https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3) * [SyRust: Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis](https://dl.acm.org/doi/10.1145/3453483.3454084) +* [Crabtree: Rust API Test Synthesis Guided by Coverage and Type](https://dl.acm.org/doi/10.1145/3689733) +* [Rustlantis: Randomized Differential Testing of the Rust Compiler](https://dl.acm.org/doi/10.1145/3689780) +* [A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries](https://arxiv.org/abs/2404.11671) +* [Tree Borrows](https://plf.inf.ethz.ch/research/pldi25-tree-borrows.html) +* [Miri: Practical Undefined Behavior Detection for Rust](https://plf.inf.ethz.ch/research/popl26-miri.html) **(this paper describes Miri itself)** ## License diff --git a/src/tools/miri/doc/genmc.md b/src/tools/miri/doc/genmc.md index 7da7a3d189487..e9d4849bc5960 100644 --- a/src/tools/miri/doc/genmc.md +++ b/src/tools/miri/doc/genmc.md @@ -1,7 +1,6 @@ # **(WIP)** Documentation for Miri-GenMC -**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).** - +**NOTE: GenMC mode is not yet fully implemented, and has [several correctness issues](https://github.com/rust-lang/miri/issues/4572) and [other limitations](#limitations). Using GenMC mode currently requires manually compiling Miri, see [Usage](#usage).** [GenMC](https://github.com/MPI-SWS/genmc) is a stateless model checker for exploring concurrent executions of a program. Miri-GenMC integrates that model checker into Miri. @@ -12,11 +11,14 @@ This includes all possible thread interleavings and all allowed return values fo It is hence still possible to have latent bugs in a test case even if they passed GenMC.) GenMC requires the input program to be bounded, i.e., have finitely many possible executions, otherwise it will not terminate. -Any loops that may run infinitely must be replaced or bounded (see below). +Any loops that may run infinitely must be replaced or bounded (see [below](#eliminating-unbounded-loops)). GenMC makes use of Dynamic Partial Order Reduction (DPOR) to reduce the number of executions that must be explored, but the runtime can still be super-exponential in the size of the input program (number of threads and amount of interaction between threads). Large programs may not be verifiable in a reasonable amount of time. +GenMC currently only supports Linux hosts. +Both the host and the target must be 64-bit little-endian. + ## Usage For testing/developing Miri-GenMC: @@ -50,16 +52,24 @@ Note that `cargo miri test` in GenMC mode is currently not supported. - `debug2`: Print the execution graph after every memory access. - `debug3`: Print reads-from values considered by GenMC. - `-Zmiri-genmc-verbose`: Show more information, such as estimated number of executions, and time taken for verification. - -#### Regular Miri parameters useful for GenMC mode - - `-Zmiri-disable-weak-memory-emulation`: Disable any weak memory effects (effectively upgrading all atomic orderings in the program to `SeqCst`). This option may reduce the number of explored program executions, but any bugs related to weak memory effects will be missed. This option can help determine if an error is caused by weak memory effects (i.e., if it disappears with this option enabled). -## Tips +## Limitations + +There are several limitations which can make GenMC miss bugs: +- GenMC does not support re-using freed memory for new allocations, so any bugs related to that will be missed. +- GenMC does not support `compare_exchange_weak`, so the consequences of spurious failures are not explored. + A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies). +- GenMC does not support the separate failure ordering of `compare_exchange`. Miri will take the maximum of the success and failure ordering and use that for the access; outcomes that rely on the real ordering being weaker will not be explored. + A warning will be emitted if this affects code you wrote (but not if it happens inside your dependencies). +- GenMC is incompatible with borrow tracking (Stacked/Tree Borrows). You need to set `-Zmiri-disable-stacked-borrows` to use GenMC. +- Like all C++ memory model verification tools, GenMC has to solve the [out-of-thin-air problem](https://www.cl.cam.ac.uk/~pes20/cpp/notes42.html). + It takes the [usual approach](https://plv.mpi-sws.org/scfix/paper.pdf) of requiring the union of "program-order" and "reads-from" to be acyclic. + This means it excludes certain behaviors allowed by the C++ memory model, some of which can occur on hardware that performs load buffering. - +## Tips ### Eliminating unbounded loops @@ -121,24 +131,11 @@ fn count_until_true_genmc(flag: &AtomicBool) -> u64 { -## Limitations - -Some or all of these limitations might get removed in the future: - -- Borrow tracking is currently incompatible (stacked/tree borrows). -- Only Linux is supported for now. -- No support for 32-bit or big-endian targets. -- No cross-target interpretation. - - - ## Development GenMC is written in C++, which complicates development a bit. The prerequisites for building Miri-GenMC are: -- A compiler with C++23 support. -- LLVM developments headers and clang. - +- A compiler with sufficient C++20 support (we are testing GCC 13). The actual code for GenMC is not contained in the Miri repo itself, but in a [separate GenMC repo](https://github.com/MPI-SWS/genmc) (with its own maintainers). These sources need to be available to build Miri-GenMC. @@ -149,6 +146,8 @@ The process for obtaining them is as follows: If you place this directory inside the Miri folder, it is recommended to call it `genmc-src` as that tells `./miri fmt` to avoid formatting the Rust files inside that folder. + + ### Formatting the C++ code For formatting the C++ code we provide a `.clang-format` file in the `genmc-sys` directory. @@ -157,7 +156,3 @@ With `clang-format` installed, run this command to format the c++ files (replace find ./genmc-sys/cpp/ -name "*.cpp" -o -name "*.hpp" | xargs clang-format --style=file:"./genmc-sys/.clang-format" -i ``` NOTE: this is currently not done automatically on pull requests to Miri. - - - - diff --git a/src/tools/miri/rust-version b/src/tools/miri/rust-version index b6a1415f1834c..e79ad9362c085 100644 --- a/src/tools/miri/rust-version +++ b/src/tools/miri/rust-version @@ -1 +1 @@ -36b2369c91d32c2659887ed6fe3d570640f44fd2 +dc47a69ed94bc88b10b7d500cceacf29b87bcbbe diff --git a/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs index e8d97491acaf3..a21898c506ab9 100644 --- a/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs +++ b/src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs @@ -826,15 +826,12 @@ trait EvalContextPrivExt<'tcx, 'ecx>: crate::MiriInterpCxExt<'tcx> { // FIXME: If we cannot determine the size (because the unsized tail is an `extern type`), // bail out -- we cannot reasonably figure out which memory range to reborrow. // See https://github.com/rust-lang/unsafe-code-guidelines/issues/276. - let size = match size { - Some(size) => size, - None => { - static DEDUP: AtomicBool = AtomicBool::new(false); - if !DEDUP.swap(true, std::sync::atomic::Ordering::Relaxed) { - this.emit_diagnostic(NonHaltingDiagnostic::ExternTypeReborrow); - } - return interp_ok(place.clone()); + let Some(size) = size else { + static DEDUP: AtomicBool = AtomicBool::new(false); + if !DEDUP.swap(true, std::sync::atomic::Ordering::Relaxed) { + this.emit_diagnostic(NonHaltingDiagnostic::ExternTypeReborrow); } + return interp_ok(place.clone()); }; // Compute new borrow. diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs index a91f35a9dcad3..055baca8542fd 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs @@ -77,6 +77,32 @@ pub struct Event { pub span: Span, } +/// Diagnostics data about the current access and the location we are accessing. +/// Used to create history events and errors. +#[derive(Clone, Debug)] +pub struct DiagnosticInfo { + pub alloc_id: AllocId, + pub span: Span, + /// The range the diagnostic actually applies to. + /// This is always a subset of `access_range`. + pub transition_range: Range, + /// The range the access is happening to. Is `None` if this is the protector release access + pub access_range: Option, + pub access_cause: AccessCause, +} +impl DiagnosticInfo { + /// Creates a history event. + pub fn create_event(&self, transition: PermTransition, is_foreign: bool) -> Event { + Event { + transition, + is_foreign, + access_cause: self.access_cause, + access_range: self.access_range, + transition_range: self.transition_range.clone(), + span: self.span, + } + } +} /// List of all events that affected a tag. /// NOTE: not all of these events are relevant for a particular location, /// the events should be filtered before the generation of diagnostics. @@ -280,32 +306,29 @@ impl History { pub(super) struct TbError<'node> { /// What failure occurred. pub error_kind: TransitionError, - /// The allocation in which the error is happening. - pub alloc_id: AllocId, - /// The offset (into the allocation) at which the conflict occurred. - pub error_offset: u64, + /// Diagnostic data about the access that caused the error. + pub access_info: &'node DiagnosticInfo, /// The tag on which the error was triggered. /// On protector violations, this is the tag that was protected. /// On accesses rejected due to insufficient permissions, this is the /// tag that lacked those permissions. - pub conflicting_info: &'node NodeDebugInfo, - // What kind of access caused this error (read, write, reborrow, deallocation) - pub access_cause: AccessCause, + pub conflicting_node_info: &'node NodeDebugInfo, /// Which tag, if any, the access that caused this error was made through, i.e. /// which tag was used to read/write/deallocate. /// Not set on wildcard accesses. - pub accessed_info: Option<&'node NodeDebugInfo>, + pub accessed_node_info: Option<&'node NodeDebugInfo>, } impl TbError<'_> { /// Produce a UB error. pub fn build<'tcx>(self) -> InterpErrorKind<'tcx> { use TransitionError::*; - let cause = self.access_cause; - let accessed = self.accessed_info; + let cause = self.access_info.access_cause; + let error_offset = self.access_info.transition_range.start; + let accessed = self.accessed_node_info; let accessed_str = - self.accessed_info.map(|v| format!("{v}")).unwrap_or_else(|| "".into()); - let conflicting = self.conflicting_info; + self.accessed_node_info.map(|v| format!("{v}")).unwrap_or_else(|| "".into()); + let conflicting = self.conflicting_node_info; // An access is considered conflicting if it happened through a // different tag than the one who caused UB. // When doing a wildcard access (where `accessed` is `None`) we @@ -316,9 +339,8 @@ impl TbError<'_> { // all tags through which an access would cause UB. let accessed_is_conflicting = accessed.map(|a| a.tag) == Some(conflicting.tag); let title = format!( - "{cause} through {accessed_str} at {alloc_id:?}[{offset:#x}] is forbidden", - alloc_id = self.alloc_id, - offset = self.error_offset + "{cause} through {accessed_str} at {alloc_id:?}[{error_offset:#x}] is forbidden", + alloc_id = self.access_info.alloc_id ); let (title, details, conflicting_tag_name) = match self.error_kind { ChildAccessForbidden(perm) => { @@ -362,13 +384,13 @@ impl TbError<'_> { } }; let mut history = HistoryData::default(); - if let Some(accessed_info) = self.accessed_info + if let Some(accessed_info) = self.accessed_node_info && !accessed_is_conflicting { history.extend(accessed_info.history.forget(), "accessed", false); } history.extend( - self.conflicting_info.history.extract_relevant(self.error_offset, self.error_kind), + self.conflicting_node_info.history.extract_relevant(error_offset, self.error_kind), conflicting_tag_name, true, ); @@ -379,12 +401,12 @@ impl TbError<'_> { /// Cannot access this allocation with wildcard provenance, as there are no /// valid exposed references for this access kind. pub fn no_valid_exposed_references_error<'tcx>( - alloc_id: AllocId, - offset: u64, - access_cause: AccessCause, + DiagnosticInfo { alloc_id, transition_range, access_cause, .. }: &DiagnosticInfo, ) -> InterpErrorKind<'tcx> { - let title = - format!("{access_cause} through at {alloc_id:?}[{offset:#x}] is forbidden"); + let title = format!( + "{access_cause} through at {alloc_id:?}[{offset:#x}] is forbidden", + offset = transition_range.start + ); let details = vec![format!("there are no exposed tags which may perform this access here")]; let history = HistoryData::default(); err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, details, history }) diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs index 018421ad1064f..173145788ee39 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs @@ -60,7 +60,9 @@ impl<'tcx> Tree { let span = machine.current_user_relevant_span(); self.perform_access( prov, - Some((range, access_kind, diagnostics::AccessCause::Explicit(access_kind))), + range, + access_kind, + diagnostics::AccessCause::Explicit(access_kind), global, alloc_id, span, @@ -94,8 +96,7 @@ impl<'tcx> Tree { alloc_id: AllocId, // diagnostics ) -> InterpResult<'tcx> { let span = machine.current_user_relevant_span(); - // `None` makes it the magic on-protector-end operation - self.perform_access(ProvenanceExtra::Concrete(tag), None, global, alloc_id, span)?; + self.perform_protector_end_access(tag, global, alloc_id, span)?; self.update_exposure_for_protector_release(tag); @@ -219,26 +220,18 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { }; trace!("Reborrow of size {:?}", ptr_size); - let (alloc_id, base_offset, parent_prov) = match this.ptr_try_get_alloc_id(place.ptr(), 0) { - Ok(data) => { - // Unlike SB, we *do* a proper retag for size 0 if can identify the allocation. - // After all, the pointer may be lazily initialized outside this initial range. - data - } - Err(_) => { - assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here - // This pointer doesn't come with an AllocId, so there's no - // memory to do retagging in. - let new_prov = place.ptr().provenance; - trace!( - "reborrow of size 0: reusing {:?} (pointee {})", - place.ptr(), - place.layout.ty, - ); - log_creation(this, None)?; - // Keep original provenance. - return interp_ok(new_prov); - } + // Unlike SB, we *do* a proper retag for size 0 if can identify the allocation. + // After all, the pointer may be lazily initialized outside this initial range. + let Ok((alloc_id, base_offset, parent_prov)) = this.ptr_try_get_alloc_id(place.ptr(), 0) + else { + assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here + // This pointer doesn't come with an AllocId, so there's no + // memory to do retagging in. + let new_prov = place.ptr().provenance; + trace!("reborrow of size 0: reusing {:?} (pointee {})", place.ptr(), place.layout.ty,); + log_creation(this, None)?; + // Keep original provenance. + return interp_ok(new_prov); }; let new_prov = Provenance::Concrete { alloc_id, tag: new_tag }; @@ -344,7 +337,9 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { tree_borrows.perform_access( parent_prov, - Some((range_in_alloc, AccessKind::Read, diagnostics::AccessCause::Reborrow)), + range_in_alloc, + AccessKind::Read, + diagnostics::AccessCause::Reborrow, this.machine.borrow_tracker.as_ref().unwrap(), alloc_id, this.machine.current_user_relevant_span(), @@ -609,8 +604,12 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { let this = self.eval_context_mut(); let (tag, alloc_id) = match ptr.provenance { Some(Provenance::Concrete { tag, alloc_id }) => (tag, alloc_id), - _ => { - eprintln!("Can't give the name {name} to Wildcard pointer"); + Some(Provenance::Wildcard) => { + eprintln!("Can't give the name {name} to wildcard pointer"); + return interp_ok(()); + } + None => { + eprintln!("Can't give the name {name} to pointer without provenance"); return interp_ok(()); } }; diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs index ca68dc8910200..900e9c3729c84 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs @@ -18,12 +18,12 @@ use rustc_data_structures::fx::FxHashSet; use rustc_span::Span; use smallvec::SmallVec; -use super::Permission; use super::diagnostics::{ - self, AccessCause, NodeDebugInfo, TbError, TransitionError, no_valid_exposed_references_error, + AccessCause, DiagnosticInfo, NodeDebugInfo, TbError, TransitionError, + no_valid_exposed_references_error, }; use super::foreign_access_skipping::IdempotentForeignAccess; -use super::perms::PermTransition; +use super::perms::{PermTransition, Permission}; use super::tree_visitor::{ChildrenVisitMode, ContinueTraversal, NodeAppArgs, TreeVisitor}; use super::unimap::{UniIndex, UniKeyMap, UniValMap}; use super::wildcard::WildcardState; @@ -91,12 +91,9 @@ impl LocationState { nodes: &mut UniValMap, wildcard_accesses: &mut UniValMap, access_kind: AccessKind, - access_cause: AccessCause, //diagnostics - access_range: Option, //diagnostics relatedness: AccessRelatedness, - span: Span, //diagnostics - location_range: Range, //diagnostics protected: bool, + diagnostics: &DiagnosticInfo, ) -> Result<(), TransitionError> { // Call this function now (i.e. only if we know `relatedness`), which // ensures it is only called when `skip_if_known_noop` returns @@ -107,14 +104,9 @@ impl LocationState { if !transition.is_noop() { let node = nodes.get_mut(idx).unwrap(); // Record the event as part of the history. - node.debug_info.history.push(diagnostics::Event { - transition, - is_foreign: relatedness.is_foreign(), - access_cause, - access_range, - transition_range: location_range, - span, - }); + node.debug_info + .history + .push(diagnostics.create_event(transition, relatedness.is_foreign())); // We need to update the wildcard state, if the permission // of an exposed pointer changes. @@ -544,7 +536,9 @@ impl<'tcx> Tree { ) -> InterpResult<'tcx> { self.perform_access( prov, - Some((access_range, AccessKind::Write, diagnostics::AccessCause::Dealloc)), + access_range, + AccessKind::Write, + AccessCause::Dealloc, global, alloc_id, span, @@ -558,6 +552,13 @@ impl<'tcx> Tree { // Check if this breaks any strong protector. // (Weak protectors are already handled by `perform_access`.) for (loc_range, loc) in self.locations.iter_mut(access_range.start, access_range.size) { + let diagnostics = DiagnosticInfo { + alloc_id, + span, + transition_range: loc_range, + access_range: Some(access_range), + access_cause: AccessCause::Dealloc, + }; // Checks the tree containing `idx` for strong protector violations. // It does this in traversal order. let mut check_tree = |idx| { @@ -584,12 +585,10 @@ impl<'tcx> Tree { && perm.accessed { Err(TbError { - conflicting_info: &node.debug_info, - access_cause: diagnostics::AccessCause::Dealloc, - alloc_id, - error_offset: loc_range.start, error_kind: TransitionError::ProtectedDealloc, - accessed_info: start_idx + access_info: &diagnostics, + conflicting_node_info: &node.debug_info, + accessed_node_info: start_idx .map(|idx| &args.nodes.get(idx).unwrap().debug_info), } .build()) @@ -620,14 +619,6 @@ impl<'tcx> Tree { /// to each location of the first component of `access_range_and_kind`, /// on every tag of the allocation. /// - /// If `access_range_and_kind` is `None`, this is interpreted as the special - /// access that is applied on protector release: - /// - the access will be applied only to accessed locations of the allocation, - /// - it will not be visible to children, - /// - it will be recorded as a `FnExit` diagnostic access - /// - and it will be a read except if the location is `Unique`, i.e. has been written to, - /// in which case it will be a write. - /// /// `LocationState::perform_access` will take care of raising transition /// errors and updating the `accessed` status of each location, /// this traversal adds to that: @@ -637,7 +628,9 @@ impl<'tcx> Tree { pub fn perform_access( &mut self, prov: ProvenanceExtra, - access_range_and_kind: Option<(AllocRange, AccessKind, diagnostics::AccessCause)>, + access_range: AllocRange, + access_kind: AccessKind, + access_cause: AccessCause, // diagnostics global: &GlobalState, alloc_id: AllocId, // diagnostics span: Span, // diagnostics @@ -651,61 +644,80 @@ impl<'tcx> Tree { ProvenanceExtra::Concrete(tag) => Some(self.tag_mapping.get(&tag).unwrap()), ProvenanceExtra::Wildcard => None, }; - if let Some((access_range, access_kind, access_cause)) = access_range_and_kind { - // Default branch: this is a "normal" access through a known range. - // We iterate over affected locations and traverse the tree for each of them. - for (loc_range, loc) in self.locations.iter_mut(access_range.start, access_range.size) { + // We iterate over affected locations and traverse the tree for each of them. + for (loc_range, loc) in self.locations.iter_mut(access_range.start, access_range.size) { + let diagnostics = DiagnosticInfo { + access_cause, + access_range: Some(access_range), + alloc_id, + span, + transition_range: loc_range, + }; + loc.perform_access( + self.roots.iter().copied(), + &mut self.nodes, + source_idx, + access_kind, + global, + ChildrenVisitMode::VisitChildrenOfAccessed, + &diagnostics, + )?; + } + interp_ok(()) + } + /// This is the special access that is applied on protector release: + /// - the access will be applied only to accessed locations of the allocation, + /// - it will not be visible to children, + /// - it will be recorded as a `FnExit` diagnostic access + /// - and it will be a read except if the location is `Unique`, i.e. has been written to, + /// in which case it will be a write. + /// - otherwise identical to `Tree::perform_access` + pub fn perform_protector_end_access( + &mut self, + tag: BorTag, + global: &GlobalState, + alloc_id: AllocId, // diagnostics + span: Span, // diagnostics + ) -> InterpResult<'tcx> { + #[cfg(feature = "expensive-consistency-checks")] + if self.roots.len() > 1 { + self.verify_wildcard_consistency(global); + } + + let source_idx = self.tag_mapping.get(&tag).unwrap(); + + // This is a special access through the entire allocation. + // It actually only affects `accessed` locations, so we need + // to filter on those before initiating the traversal. + // + // In addition this implicit access should not be visible to children, + // thus the use of `traverse_nonchildren`. + // See the test case `returned_mut_is_usable` from + // `tests/pass/tree_borrows/tree-borrows.rs` for an example of + // why this is important. + for (loc_range, loc) in self.locations.iter_mut_all() { + // Only visit accessed permissions + if let Some(p) = loc.perms.get(source_idx) + && let Some(access_kind) = p.permission.protector_end_access() + && p.accessed + { + let diagnostics = DiagnosticInfo { + access_cause: AccessCause::FnExit(access_kind), + access_range: None, + alloc_id, + span, + transition_range: loc_range, + }; loc.perform_access( self.roots.iter().copied(), &mut self.nodes, - source_idx, - loc_range, - Some(access_range), + Some(source_idx), access_kind, - access_cause, global, - alloc_id, - span, - ChildrenVisitMode::VisitChildrenOfAccessed, + ChildrenVisitMode::SkipChildrenOfAccessed, + &diagnostics, )?; } - } else { - // This is a special access through the entire allocation. - // It actually only affects `accessed` locations, so we need - // to filter on those before initiating the traversal. - // - // In addition this implicit access should not be visible to children, - // thus the use of `traverse_nonchildren`. - // See the test case `returned_mut_is_usable` from - // `tests/pass/tree_borrows/tree-borrows.rs` for an example of - // why this is important. - - // Wildcard references are never protected. So this can never be - // called with a wildcard reference. - let source_idx = source_idx.unwrap(); - - for (loc_range, loc) in self.locations.iter_mut_all() { - // Only visit accessed permissions - if let Some(p) = loc.perms.get(source_idx) - && let Some(access_kind) = p.permission.protector_end_access() - && p.accessed - { - let access_cause = diagnostics::AccessCause::FnExit(access_kind); - loc.perform_access( - self.roots.iter().copied(), - &mut self.nodes, - Some(source_idx), - loc_range, - None, - access_kind, - access_cause, - global, - alloc_id, - span, - ChildrenVisitMode::SkipChildrenOfAccessed, - )?; - } - } } interp_ok(()) } @@ -872,27 +884,19 @@ impl<'tcx> LocationTree { roots: impl Iterator, nodes: &mut UniValMap, access_source: Option, - loc_range: Range, // diagnostics - access_range: Option, // diagnostics access_kind: AccessKind, - access_cause: diagnostics::AccessCause, // diagnostics global: &GlobalState, - alloc_id: AllocId, // diagnostics - span: Span, // diagnostics visit_children: ChildrenVisitMode, + diagnostics: &DiagnosticInfo, ) -> InterpResult<'tcx> { let accessed_root = if let Some(idx) = access_source { Some(self.perform_normal_access( idx, nodes, - loc_range.clone(), - access_range, access_kind, - access_cause, global, - alloc_id, - span, visit_children, + diagnostics, )?) } else { // `SkipChildrenOfAccessed` only gets set on protector release, which only @@ -926,13 +930,9 @@ impl<'tcx> LocationTree { access_source, /*max_local_tag*/ accessed_root_tag, nodes, - loc_range.clone(), - access_range, access_kind, - access_cause, global, - alloc_id, - span, + diagnostics, )?; } interp_ok(()) @@ -948,14 +948,10 @@ impl<'tcx> LocationTree { &mut self, access_source: UniIndex, nodes: &mut UniValMap, - loc_range: Range, // diagnostics - access_range: Option, // diagnostics access_kind: AccessKind, - access_cause: diagnostics::AccessCause, // diagnostics global: &GlobalState, - alloc_id: AllocId, // diagnostics - span: Span, // diagnostics visit_children: ChildrenVisitMode, + diagnostics: &DiagnosticInfo, ) -> InterpResult<'tcx, UniIndex> { // Performs the per-node work: // - insert the permission if it does not exist @@ -987,21 +983,18 @@ impl<'tcx> LocationTree { args.nodes, &mut args.data.wildcard_accesses, access_kind, - access_cause, - access_range, args.rel_pos, - span, - loc_range.clone(), protected, + diagnostics, ) .map_err(|error_kind| { TbError { - conflicting_info: &args.nodes.get(args.idx).unwrap().debug_info, - access_cause, - alloc_id, - error_offset: loc_range.start, error_kind, - accessed_info: Some(&args.nodes.get(access_source).unwrap().debug_info), + access_info: diagnostics, + conflicting_node_info: &args.nodes.get(args.idx).unwrap().debug_info, + accessed_node_info: Some( + &args.nodes.get(access_source).unwrap().debug_info, + ), } .build() }) @@ -1030,13 +1023,9 @@ impl<'tcx> LocationTree { access_source: Option, max_local_tag: Option, nodes: &mut UniValMap, - loc_range: Range, // diagnostics - access_range: Option, // diagnostics access_kind: AccessKind, - access_cause: diagnostics::AccessCause, // diagnostics global: &GlobalState, - alloc_id: AllocId, // diagnostics - span: Span, // diagnostics + diagnostics: &DiagnosticInfo, ) -> InterpResult<'tcx> { let get_relatedness = |idx: UniIndex, node: &Node, loc: &LocationTree| { let wildcard_state = loc.wildcard_accesses.get(idx).cloned().unwrap_or_default(); @@ -1090,11 +1079,7 @@ impl<'tcx> LocationTree { // This can only happen if `root` is the main root: We set // `max_foreign_access==Write` on all wildcard roots, so at least a foreign access // is always possible on all nodes in a wildcard subtree. - return Err(no_valid_exposed_references_error( - alloc_id, - loc_range.start, - access_cause, - )); + return Err(no_valid_exposed_references_error(diagnostics)); }; let Some(relatedness) = wildcard_relatedness.to_relatedness() else { @@ -1113,22 +1098,17 @@ impl<'tcx> LocationTree { args.nodes, &mut args.data.wildcard_accesses, access_kind, - access_cause, - access_range, relatedness, - span, - loc_range.clone(), protected, + diagnostics, ) .map_err(|trans| { let node = args.nodes.get(args.idx).unwrap(); TbError { - conflicting_info: &node.debug_info, - access_cause, - alloc_id, - error_offset: loc_range.start, error_kind: trans, - accessed_info: access_source + access_info: diagnostics, + conflicting_node_info: &node.debug_info, + accessed_node_info: access_source .map(|idx| &args.nodes.get(idx).unwrap().debug_info), } .build() diff --git a/src/tools/miri/src/concurrency/genmc/helper.rs b/src/tools/miri/src/concurrency/genmc/helper.rs index ae16898106d86..f539e783fd3f5 100644 --- a/src/tools/miri/src/concurrency/genmc/helper.rs +++ b/src/tools/miri/src/concurrency/genmc/helper.rs @@ -171,11 +171,8 @@ impl AtomicRwOrd { (AtomicReadOrd::Acquire, AtomicWriteOrd::Relaxed) => AtomicRwOrd::Acquire, (AtomicReadOrd::Relaxed, AtomicWriteOrd::Release) => AtomicRwOrd::Release, (AtomicReadOrd::Acquire, AtomicWriteOrd::Release) => AtomicRwOrd::AcqRel, - (AtomicReadOrd::SeqCst, AtomicWriteOrd::SeqCst) => AtomicRwOrd::SeqCst, - _ => - panic!( - "Unsupported memory ordering combination ({read_ordering:?}, {write_ordering:?})" - ), + (AtomicReadOrd::SeqCst, _) => AtomicRwOrd::SeqCst, + (_, AtomicWriteOrd::SeqCst) => AtomicRwOrd::SeqCst, } } diff --git a/src/tools/miri/src/concurrency/genmc/mod.rs b/src/tools/miri/src/concurrency/genmc/mod.rs index 73da0e11daaf7..36b1d2afade4f 100644 --- a/src/tools/miri/src/concurrency/genmc/mod.rs +++ b/src/tools/miri/src/concurrency/genmc/mod.rs @@ -402,8 +402,20 @@ impl GenmcCtx { // FIXME(genmc): remove once GenMC supports failure memory ordering in `compare_exchange`. let (effective_failure_ordering, _) = upgraded_success_ordering.split_memory_orderings(); - // Return a warning if the actual orderings don't match the upgraded ones. - if success != upgraded_success_ordering || effective_failure_ordering != fail { + + // Return a warning if we cannot explore all behaviors of this operation. + // Only emit this if the operation is "in user code": walk up across `#[track_caller]` + // frames, then check if the next frame is local. + let show_warning = || { + ecx.active_thread_stack() + .iter() + .rev() + .find(|f| !f.instance().def.requires_caller_location(*ecx.tcx)) + .is_none_or(|f| ecx.machine.is_local(f.instance())) + }; + if (success != upgraded_success_ordering || effective_failure_ordering != fail) + && show_warning() + { static DEDUP: SpanDedupDiagnostic = SpanDedupDiagnostic::new(); ecx.dedup_diagnostic(&DEDUP, |_first| { NonHaltingDiagnostic::GenmcCompareExchangeOrderingMismatch { @@ -415,7 +427,7 @@ impl GenmcCtx { }); } // FIXME(genmc): remove once GenMC implements spurious failures for `compare_exchange_weak`. - if can_fail_spuriously { + if can_fail_spuriously && show_warning() { static DEDUP: SpanDedupDiagnostic = SpanDedupDiagnostic::new(); ecx.dedup_diagnostic(&DEDUP, |_first| NonHaltingDiagnostic::GenmcCompareExchangeWeak); } diff --git a/src/tools/miri/src/concurrency/thread.rs b/src/tools/miri/src/concurrency/thread.rs index 5016e3b66ca6a..1c404d419ef83 100644 --- a/src/tools/miri/src/concurrency/thread.rs +++ b/src/tools/miri/src/concurrency/thread.rs @@ -834,7 +834,7 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> { // sleep until the first callback. interp_ok(SchedulingAction::Sleep(sleep_time)) } else { - throw_machine_stop!(TerminationInfo::Deadlock); + throw_machine_stop!(TerminationInfo::GlobalDeadlock); } } } diff --git a/src/tools/miri/src/concurrency/weak_memory.rs b/src/tools/miri/src/concurrency/weak_memory.rs index 2255e0d48174e..6fe73fec0f57f 100644 --- a/src/tools/miri/src/concurrency/weak_memory.rs +++ b/src/tools/miri/src/concurrency/weak_memory.rs @@ -208,11 +208,10 @@ impl StoreBufferAlloc { range: AllocRange, ) -> InterpResult<'tcx, Option>> { let access_type = self.store_buffers.borrow().access_type(range); - let pos = match access_type { - AccessType::PerfectlyOverlapping(pos) => pos, + let AccessType::PerfectlyOverlapping(pos) = access_type else { // If there is nothing here yet, that means there wasn't an atomic write yet so // we can't return anything outdated. - _ => return interp_ok(None), + return interp_ok(None); }; let store_buffer = Ref::map(self.store_buffers.borrow(), |buffer| &buffer[pos]); interp_ok(Some(store_buffer)) diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs index 01f77f261d703..e53c41157a89a 100644 --- a/src/tools/miri/src/diagnostics.rs +++ b/src/tools/miri/src/diagnostics.rs @@ -32,7 +32,10 @@ pub enum TerminationInfo { history: tree_diagnostics::HistoryData, }, Int2PtrWithStrictProvenance, - Deadlock, + /// All threads are blocked. + GlobalDeadlock, + /// Some thread discovered a deadlock condition (e.g. in a mutex with reentrancy checking). + LocalDeadlock, MultipleSymbolDefinitions { link_name: Symbol, first: SpanData, @@ -76,7 +79,8 @@ impl fmt::Display for TerminationInfo { ), StackedBorrowsUb { msg, .. } => write!(f, "{msg}"), TreeBorrowsUb { title, .. } => write!(f, "{title}"), - Deadlock => write!(f, "the evaluated program deadlocked"), + GlobalDeadlock => write!(f, "the evaluated program deadlocked"), + LocalDeadlock => write!(f, "a thread deadlocked"), MultipleSymbolDefinitions { link_name, .. } => write!(f, "multiple definitions of symbol `{link_name}`"), SymbolShimClashing { link_name, .. } => @@ -245,10 +249,39 @@ pub fn report_result<'tcx>( Some("unsupported operation"), StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } => Some("Undefined Behavior"), - Deadlock => { + LocalDeadlock => { labels.push(format!("this thread got stuck here")); None } + GlobalDeadlock => { + // Global deadlocks are reported differently: just show all blocked threads. + // The "active" thread might actually be terminated, so we ignore it. + let mut any_pruned = false; + for (thread, stack) in ecx.machine.threads.all_blocked_stacks() { + let stacktrace = Frame::generate_stacktrace_from_stack(stack); + let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine); + any_pruned |= was_pruned; + report_msg( + DiagLevel::Error, + format!("the evaluated program deadlocked"), + vec![format!( + "thread `{}` got stuck here", + ecx.machine.threads.get_thread_display_name(thread) + )], + vec![], + vec![], + &stacktrace, + Some(thread), + &ecx.machine, + ) + } + if any_pruned { + ecx.tcx.dcx().note( + "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace" + ); + } + return None; + } MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None, }; #[rustfmt::skip] @@ -408,9 +441,7 @@ pub fn report_result<'tcx>( }; let stacktrace = ecx.generate_stacktrace(); - let (stacktrace, mut any_pruned) = prune_stacktrace(stacktrace, &ecx.machine); - - let mut show_all_threads = false; + let (stacktrace, pruned) = prune_stacktrace(stacktrace, &ecx.machine); // We want to dump the allocation if this is `InvalidUninitBytes`. // Since `format_interp_error` consumes `e`, we compute the outut early. @@ -425,15 +456,6 @@ pub fn report_result<'tcx>( .unwrap(); writeln!(extra, "{:?}", ecx.dump_alloc(*alloc_id)).unwrap(); } - MachineStop(info) => { - let info = info.downcast_ref::().expect("invalid MachineStop payload"); - match info { - TerminationInfo::Deadlock => { - show_all_threads = true; - } - _ => {} - } - } _ => {} } @@ -464,28 +486,8 @@ pub fn report_result<'tcx>( eprint!("{extra}"); // newlines are already in the string - if show_all_threads { - for (thread, stack) in ecx.machine.threads.all_blocked_stacks() { - if thread != ecx.active_thread() { - let stacktrace = Frame::generate_stacktrace_from_stack(stack); - let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine); - any_pruned |= was_pruned; - report_msg( - DiagLevel::Error, - format!("the evaluated program deadlocked"), - vec![format!("this thread got stuck here")], - vec![], - vec![], - &stacktrace, - Some(thread), - &ecx.machine, - ) - } - } - } - // Include a note like `std` does when we omit frames from a backtrace - if any_pruned { + if pruned { ecx.tcx.dcx().note( "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace", ); @@ -574,7 +576,7 @@ pub fn report_msg<'tcx>( err.span(span); // Show main message. - if span != DUMMY_SP { + if !span.is_dummy() { for line in span_msg { err.span_label(span, line); } diff --git a/src/tools/miri/src/eval.rs b/src/tools/miri/src/eval.rs index 01a54bbb33746..0423b0ea5abdf 100644 --- a/src/tools/miri/src/eval.rs +++ b/src/tools/miri/src/eval.rs @@ -543,9 +543,7 @@ where { // Parse argv[0]. Slashes aren't escaped. Literal double quotes are not allowed. let mut cmd = { - let arg0 = if let Some(arg0) = args.next() { - arg0 - } else { + let Some(arg0) = args.next() else { return vec![0]; }; let arg0 = arg0.as_ref(); diff --git a/src/tools/miri/src/lib.rs b/src/tools/miri/src/lib.rs index fe501b8d7b30d..9776ef825e729 100644 --- a/src/tools/miri/src/lib.rs +++ b/src/tools/miri/src/lib.rs @@ -46,7 +46,12 @@ rustc::potential_query_instability, rustc::untranslatable_diagnostic, )] -#![warn(rust_2018_idioms, unqualified_local_imports, clippy::as_conversions)] +#![warn( + rust_2018_idioms, + unqualified_local_imports, + clippy::as_conversions, + clippy::manual_let_else +)] // Needed for rustdoc from bootstrap (with `-Znormalize-docs`). #![recursion_limit = "256"] diff --git a/src/tools/miri/src/shims/backtrace.rs b/src/tools/miri/src/shims/backtrace.rs index bd3914b652ac9..1ca814ee7afff 100644 --- a/src/tools/miri/src/shims/backtrace.rs +++ b/src/tools/miri/src/shims/backtrace.rs @@ -92,21 +92,18 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { let (alloc_id, offset, _prov) = this.ptr_get_alloc_id(ptr, 0)?; // This has to be an actual global fn ptr, not a dlsym function. - let fn_instance = if let Some(GlobalAlloc::Function { instance, .. }) = - this.tcx.try_get_global_alloc(alloc_id) - { - instance - } else { + let Some(GlobalAlloc::Function { instance, .. }) = this.tcx.try_get_global_alloc(alloc_id) + else { throw_ub_format!("expected static function pointer, found {:?}", ptr); }; let lo = this.tcx.sess.source_map().lookup_char_pos(BytePos(offset.bytes().try_into().unwrap())); - let name = fn_instance.to_string(); + let name = instance.to_string(); let filename = lo.file.name.prefer_remapped_unconditionally().to_string(); - interp_ok((fn_instance, lo, name, filename)) + interp_ok((instance, lo, name, filename)) } fn handle_miri_resolve_frame( diff --git a/src/tools/miri/src/shims/native_lib/mod.rs b/src/tools/miri/src/shims/native_lib/mod.rs index 445f9618e7e36..12abe841c0528 100644 --- a/src/tools/miri/src/shims/native_lib/mod.rs +++ b/src/tools/miri/src/shims/native_lib/mod.rs @@ -459,12 +459,9 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { ) -> InterpResult<'tcx, bool> { let this = self.eval_context_mut(); // Get the pointer to the function in the shared object file if it exists. - let code_ptr = match this.get_func_ptr_explicitly_from_lib(link_name) { - Some(ptr) => ptr, - None => { - // Shared object file does not export this function -- try the shims next. - return interp_ok(false); - } + let Some(code_ptr) = this.get_func_ptr_explicitly_from_lib(link_name) else { + // Shared object file does not export this function -- try the shims next. + return interp_ok(false); }; // Do we have ptrace? diff --git a/src/tools/miri/src/shims/time.rs b/src/tools/miri/src/shims/time.rs index 614cc75c6d580..2bbae80a0b919 100644 --- a/src/tools/miri/src/shims/time.rs +++ b/src/tools/miri/src/shims/time.rs @@ -337,11 +337,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { let duration = this.deref_pointer_as(duration, this.libc_ty_layout("timespec"))?; let _rem = this.read_pointer(rem)?; // Signal handlers are not supported, so rem will never be written to. - let duration = match this.read_timespec(&duration)? { - Some(duration) => duration, - None => { - return this.set_last_error_and_return_i32(LibcError("EINVAL")); - } + let Some(duration) = this.read_timespec(&duration)? else { + return this.set_last_error_and_return_i32(LibcError("EINVAL")); }; this.block_thread( @@ -378,11 +375,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { throw_unsup_format!("clock_nanosleep: only CLOCK_MONOTONIC is supported"); } - let duration = match this.read_timespec(×pec)? { - Some(duration) => duration, - None => { - return this.set_last_error_and_return_i32(LibcError("EINVAL")); - } + let Some(duration) = this.read_timespec(×pec)? else { + return this.set_last_error_and_return_i32(LibcError("EINVAL")); }; let timeout_anchor = if flags == 0 { diff --git a/src/tools/miri/src/shims/unix/freebsd/sync.rs b/src/tools/miri/src/shims/unix/freebsd/sync.rs index bd1ee31553727..ae8a167080b90 100644 --- a/src/tools/miri/src/shims/unix/freebsd/sync.rs +++ b/src/tools/miri/src/shims/unix/freebsd/sync.rs @@ -101,12 +101,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { // `uaddr2` points to a `struct _umtx_time`. let umtx_time_place = this.ptr_to_mplace(uaddr2, umtx_time_layout); - let umtx_time = match this.read_umtx_time(&umtx_time_place)? { - Some(ut) => ut, - None => { - return this - .set_last_error_and_return(LibcError("EINVAL"), dest); - } + let Some(umtx_time) = this.read_umtx_time(&umtx_time_place)? else { + return this.set_last_error_and_return(LibcError("EINVAL"), dest); }; let anchor = if umtx_time.abs_time { @@ -122,12 +118,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { // `uaddr2` points to a `struct timespec`. let timespec = this.ptr_to_mplace(uaddr2, timespec_layout); - let duration = match this.read_timespec(×pec)? { - Some(duration) => duration, - None => { - return this - .set_last_error_and_return(LibcError("EINVAL"), dest); - } + let Some(duration) = this.read_timespec(×pec)? else { + return this.set_last_error_and_return(LibcError("EINVAL"), dest); }; // FreeBSD does not seem to document which clock is used when the timeout @@ -220,10 +212,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { let timespec_place = this.project_field(ut, FieldIdx::from_u32(0))?; // Inner `timespec` must still be valid. - let duration = match this.read_timespec(×pec_place)? { - Some(dur) => dur, - None => return interp_ok(None), - }; + let Some(duration) = this.read_timespec(×pec_place)? else { return interp_ok(None) }; let flags_place = this.project_field(ut, FieldIdx::from_u32(1))?; let flags = this.read_scalar(&flags_place)?.to_u32()?; diff --git a/src/tools/miri/src/shims/unix/fs.rs b/src/tools/miri/src/shims/unix/fs.rs index 650972be5574e..e17456c3bc0e3 100644 --- a/src/tools/miri/src/shims/unix/fs.rs +++ b/src/tools/miri/src/shims/unix/fs.rs @@ -1157,10 +1157,11 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { return this.set_last_error_and_return_i32(LibcError("EBADF")); }; - // FIXME: Support ftruncate64 for all FDs - let file = fd.downcast::().ok_or_else(|| { - err_unsup_format!("`ftruncate64` is only supported on file-backed file descriptors") - })?; + let Some(file) = fd.downcast::() else { + // The docs say that EINVAL is returned when the FD "does not reference a regular file + // or a POSIX shared memory object" (and we don't support shmem objects). + return interp_ok(this.eval_libc("EINVAL")); + }; if file.writable { if let Ok(length) = length.try_into() { @@ -1202,10 +1203,9 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { let Some(fd) = this.machine.fds.get(fd_num) else { return interp_ok(this.eval_libc("EBADF")); }; - let file = match fd.downcast::() { - Some(file_handle) => file_handle, + let Some(file) = fd.downcast::() else { // Man page specifies to return ENODEV if `fd` is not a regular file. - None => return interp_ok(this.eval_libc("ENODEV")), + return interp_ok(this.eval_libc("ENODEV")); }; if !file.writable { diff --git a/src/tools/miri/src/shims/unix/linux_like/sync.rs b/src/tools/miri/src/shims/unix/linux_like/sync.rs index 8ff7fe0a4563b..00df4ee2b2ae3 100644 --- a/src/tools/miri/src/shims/unix/linux_like/sync.rs +++ b/src/tools/miri/src/shims/unix/linux_like/sync.rs @@ -71,11 +71,8 @@ pub fn futex<'tcx>( let timeout = if ecx.ptr_is_null(timeout.ptr())? { None } else { - let duration = match ecx.read_timespec(&timeout)? { - Some(duration) => duration, - None => { - return ecx.set_last_error_and_return(LibcError("EINVAL"), dest); - } + let Some(duration) = ecx.read_timespec(&timeout)? else { + return ecx.set_last_error_and_return(LibcError("EINVAL"), dest); }; let timeout_clock = if op & futex_realtime == futex_realtime { ecx.check_no_isolation( diff --git a/src/tools/miri/src/shims/unix/sync.rs b/src/tools/miri/src/shims/unix/sync.rs index 39014f34c8972..58a612102b180 100644 --- a/src/tools/miri/src/shims/unix/sync.rs +++ b/src/tools/miri/src/shims/unix/sync.rs @@ -538,7 +538,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { throw_ub_format!( "trying to acquire default mutex already locked by the current thread" ), - MutexKind::Normal => throw_machine_stop!(TerminationInfo::Deadlock), + MutexKind::Normal => throw_machine_stop!(TerminationInfo::LocalDeadlock), MutexKind::ErrorCheck => this.eval_libc_i32("EDEADLK"), MutexKind::Recursive => { this.mutex_lock(&mutex.mutex_ref)?; @@ -887,15 +887,12 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { let mutex_ref = mutex_get_data(this, mutex_op)?.mutex_ref.clone(); // Extract the timeout. - let duration = match this + let Some(duration) = this .read_timespec(&this.deref_pointer_as(timeout_op, this.libc_ty_layout("timespec"))?)? - { - Some(duration) => duration, - None => { - let einval = this.eval_libc("EINVAL"); - this.write_scalar(einval, dest)?; - return interp_ok(()); - } + else { + let einval = this.eval_libc("EINVAL"); + this.write_scalar(einval, dest)?; + return interp_ok(()); }; let (clock, anchor) = if macos_relative_np { diff --git a/src/tools/miri/src/shims/windows/fs.rs b/src/tools/miri/src/shims/windows/fs.rs index 775c08388c078..ad22df2425af9 100644 --- a/src/tools/miri/src/shims/windows/fs.rs +++ b/src/tools/miri/src/shims/windows/fs.rs @@ -321,11 +321,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { this.windows_ty_layout("BY_HANDLE_FILE_INFORMATION"), )?; - let fd_num = if let Handle::File(fd_num) = file { - fd_num - } else { - this.invalid_handle("GetFileInformationByHandle")? - }; + let Handle::File(fd_num) = file else { this.invalid_handle("GetFileInformationByHandle")? }; let Some(desc) = this.machine.fds.get(fd_num) else { this.invalid_handle("GetFileInformationByHandle")? @@ -448,10 +444,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { throw_unsup_format!("`NtWriteFile` `Key` parameter is non-null, which is unsupported"); } - let fd = match handle { - Handle::File(fd) => fd, - _ => this.invalid_handle("NtWriteFile")?, - }; + let Handle::File(fd) = handle else { this.invalid_handle("NtWriteFile")? }; let Some(desc) = this.machine.fds.get(fd) else { this.invalid_handle("NtWriteFile")? }; @@ -561,10 +554,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { }; let io_status_info = this.project_field_named(&io_status_block, "Information")?; - let fd = match handle { - Handle::File(fd) => fd, - _ => this.invalid_handle("NtWriteFile")?, - }; + let Handle::File(fd) = handle else { this.invalid_handle("NtWriteFile")? }; let Some(desc) = this.machine.fds.get(fd) else { this.invalid_handle("NtReadFile")? }; @@ -620,10 +610,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { let new_fp_ptr = this.read_pointer(new_fp)?; let move_method = this.read_scalar(move_method)?.to_u32()?; - let fd = match file { - Handle::File(fd) => fd, - _ => this.invalid_handle("SetFilePointerEx")?, - }; + let Handle::File(fd) = file else { this.invalid_handle("SetFilePointerEx")? }; let Some(desc) = this.machine.fds.get(fd) else { throw_unsup_format!("`SetFilePointerEx` is only supported on file backed handles"); diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_deadlock.stderr b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_deadlock.stderr index c80cbf835a386..e3b0036c9aa9b 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_deadlock.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_deadlock.stderr @@ -1,14 +1,8 @@ -error: the evaluated program deadlocked - --> tests/fail-dep/concurrency/libc_pthread_mutex_deadlock.rs:LL:CC - | -LL | assert_eq!(libc::pthread_mutex_lock(lock_copy.0.get() as *mut _), 0); - | ^ this thread got stuck here - error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -23,6 +17,12 @@ LL | | }) LL | | .join() | |_______________^ +error: the evaluated program deadlocked + --> tests/fail-dep/concurrency/libc_pthread_mutex_deadlock.rs:LL:CC + | +LL | assert_eq!(libc::pthread_mutex_lock(lock_copy.0.get() as *mut _), 0); + | ^ thread `unnamed-ID` got stuck here + note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace error: aborting due to 2 previous errors diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.rs b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.rs index b88257992a5c5..3008705ebfdea 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.rs +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.rs @@ -12,6 +12,6 @@ fn main() { assert_eq!(libc::pthread_mutex_lock(&mut mutex as *mut _), 0); // A "normal" mutex properly tries to acquire the lock even if its is already held // by the current thread -- and then we deadlock. - libc::pthread_mutex_lock(&mut mutex as *mut _); //~ ERROR: the evaluated program deadlocked + libc::pthread_mutex_lock(&mut mutex as *mut _); //~ ERROR: a thread deadlocked } } diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.stderr b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.stderr index c611d0ff7b006..782322d5c32b3 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.stderr @@ -1,4 +1,4 @@ -error: the evaluated program deadlocked +error: a thread deadlocked --> tests/fail-dep/concurrency/libc_pthread_mutex_normal_reentrant.rs:LL:CC | LL | libc::pthread_mutex_lock(&mut mutex as *mut _); diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_read_write_deadlock_single_thread.stderr b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_read_write_deadlock_single_thread.stderr index 763a52963a4d5..ea8cbcada970d 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_read_write_deadlock_single_thread.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_read_write_deadlock_single_thread.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/concurrency/libc_pthread_rwlock_read_write_deadlock_single_thread.rs:LL:CC | LL | libc::pthread_rwlock_wrlock(rw.get()); - | ^ this thread got stuck here + | ^ thread `main` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock.stderr b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock.stderr index f174d387f76e3..255632870efc8 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock.stderr @@ -1,14 +1,8 @@ -error: the evaluated program deadlocked - --> tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock.rs:LL:CC - | -LL | assert_eq!(libc::pthread_rwlock_wrlock(lock_copy.0.get() as *mut _), 0); - | ^ this thread got stuck here - error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -23,6 +17,12 @@ LL | | }) LL | | .join() | |_______________^ +error: the evaluated program deadlocked + --> tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock.rs:LL:CC + | +LL | assert_eq!(libc::pthread_rwlock_wrlock(lock_copy.0.get() as *mut _), 0); + | ^ thread `unnamed-ID` got stuck here + note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace error: aborting due to 2 previous errors diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock_single_thread.stderr b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock_single_thread.stderr index 4c8d3fddb97c2..0208a5bae4f52 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock_single_thread.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock_single_thread.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/concurrency/libc_pthread_rwlock_write_read_deadlock_single_thread.rs:LL:CC | LL | libc::pthread_rwlock_rdlock(rw.get()); - | ^ this thread got stuck here + | ^ thread `main` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock.stderr b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock.stderr index 06b8e1246e016..6891b989d05f8 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock.stderr @@ -1,14 +1,8 @@ -error: the evaluated program deadlocked - --> tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock.rs:LL:CC - | -LL | assert_eq!(libc::pthread_rwlock_wrlock(lock_copy.0.get() as *mut _), 0); - | ^ this thread got stuck here - error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -23,6 +17,12 @@ LL | | }) LL | | .join() | |_______________^ +error: the evaluated program deadlocked + --> tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock.rs:LL:CC + | +LL | assert_eq!(libc::pthread_rwlock_wrlock(lock_copy.0.get() as *mut _), 0); + | ^ thread `unnamed-ID` got stuck here + note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace error: aborting due to 2 previous errors diff --git a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock_single_thread.stderr b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock_single_thread.stderr index e6a4b2814d83c..314e60b023607 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock_single_thread.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock_single_thread.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/concurrency/libc_pthread_rwlock_write_write_deadlock_single_thread.rs:LL:CC | LL | libc::pthread_rwlock_wrlock(rw.get()); - | ^ this thread got stuck here + | ^ thread `main` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/concurrency/windows_join_main.stderr b/src/tools/miri/tests/fail-dep/concurrency/windows_join_main.stderr index 0ab89676db370..d9cc93d0fc495 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/windows_join_main.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/windows_join_main.stderr @@ -1,16 +1,8 @@ -error: the evaluated program deadlocked - --> tests/fail-dep/concurrency/windows_join_main.rs:LL:CC - | -LL | assert_eq!(WaitForSingleObject(MAIN_THREAD, INFINITE), WAIT_OBJECT_0); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this thread got stuck here - | - = note: this error originates in the macro `assert_eq` (in Nightly builds, run with -Z macro-backtrace for more info) - error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let rc = unsafe { c::WaitForSingleObject(self.handle.as_raw_handle(), c::INFINITE) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -26,6 +18,14 @@ LL | | assert_eq!(WaitForSingleObject(MAIN_THREAD, INFINITE), WAIT_O LL | | .join() | |___________^ +error: the evaluated program deadlocked + --> tests/fail-dep/concurrency/windows_join_main.rs:LL:CC + | +LL | assert_eq!(WaitForSingleObject(MAIN_THREAD, INFINITE), WAIT_OBJECT_0); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ thread `unnamed-ID` got stuck here + | + = note: this error originates in the macro `assert_eq` (in Nightly builds, run with -Z macro-backtrace for more info) + note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace error: aborting due to 2 previous errors diff --git a/src/tools/miri/tests/fail-dep/concurrency/windows_join_self.stderr b/src/tools/miri/tests/fail-dep/concurrency/windows_join_self.stderr index bdfab966d6d98..f5515983da2b4 100644 --- a/src/tools/miri/tests/fail-dep/concurrency/windows_join_self.stderr +++ b/src/tools/miri/tests/fail-dep/concurrency/windows_join_self.stderr @@ -1,14 +1,8 @@ -error: the evaluated program deadlocked - --> tests/fail-dep/concurrency/windows_join_self.rs:LL:CC - | -LL | assert_eq!(WaitForSingleObject(native, INFINITE), WAIT_OBJECT_0); - | ^ this thread got stuck here - error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let rc = unsafe { c::WaitForSingleObject(self.handle.as_raw_handle(), c::INFINITE) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -26,6 +20,12 @@ LL | | }) LL | | .join() | |___________^ +error: the evaluated program deadlocked + --> tests/fail-dep/concurrency/windows_join_self.rs:LL:CC + | +LL | assert_eq!(WaitForSingleObject(native, INFINITE), WAIT_OBJECT_0); + | ^ thread `unnamed-ID` got stuck here + note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace error: aborting due to 2 previous errors diff --git a/src/tools/miri/tests/fail-dep/libc/eventfd_block_read_twice.stderr b/src/tools/miri/tests/fail-dep/libc/eventfd_block_read_twice.stderr index 6253fe6d2c768..53ae7ea82bd95 100644 --- a/src/tools/miri/tests/fail-dep/libc/eventfd_block_read_twice.stderr +++ b/src/tools/miri/tests/fail-dep/libc/eventfd_block_read_twice.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -18,7 +18,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/libc/eventfd_block_read_twice.rs:LL:CC | LL | let res: i64 = unsafe { libc::read(fd, buf.as_mut_ptr().cast(), 8).try_into().unwrap() }; - | ^ this thread got stuck here + | ^ thread `unnamed-ID` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/libc/eventfd_block_write_twice.stderr b/src/tools/miri/tests/fail-dep/libc/eventfd_block_write_twice.stderr index aecc54c2fd882..62810f17be887 100644 --- a/src/tools/miri/tests/fail-dep/libc/eventfd_block_write_twice.stderr +++ b/src/tools/miri/tests/fail-dep/libc/eventfd_block_write_twice.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -18,7 +18,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/libc/eventfd_block_write_twice.rs:LL:CC | LL | libc::write(fd, sized_8_data.as_ptr() as *const libc::c_void, 8).try_into().unwrap() - | ^ this thread got stuck here + | ^ thread `unnamed-ID` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.rs b/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.rs index cfebb7c643512..c7a2c5b4d2973 100644 --- a/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.rs +++ b/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.rs @@ -1,5 +1,4 @@ //@ignore-target: windows # Sockets/pipes are not implemented yet -//~^ ERROR: the evaluated program deadlocked //@compile-flags: -Zmiri-deterministic-concurrency use std::thread; diff --git a/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.stderr b/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.stderr index e451fdb9d19f2..307762fb12c63 100644 --- a/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.stderr +++ b/src/tools/miri/tests/fail-dep/libc/fcntl_fsetfl_while_blocking.stderr @@ -1,15 +1,10 @@ -error: the evaluated program deadlocked - | - = note: this thread got stuck here - = note: (no span available) - error: the evaluated program deadlocked --> tests/fail-dep/libc/fcntl_fsetfl_while_blocking.rs:LL:CC | LL | let _res = unsafe { libc::read(fds[0], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace -error: aborting due to 2 previous errors +error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/fail-dep/libc/libc_epoll_block_two_thread.stderr b/src/tools/miri/tests/fail-dep/libc/libc_epoll_block_two_thread.stderr index 14390d632738d..dba12d1903170 100644 --- a/src/tools/miri/tests/fail-dep/libc/libc_epoll_block_two_thread.stderr +++ b/src/tools/miri/tests/fail-dep/libc/libc_epoll_block_two_thread.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -18,7 +18,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/libc/libc_epoll_block_two_thread.rs:LL:CC | LL | check_epoll_wait::(epfd, &expected, -1); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this thread got stuck here + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ thread `unnamed-ID` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/libc/socketpair-close-while-blocked.stderr b/src/tools/miri/tests/fail-dep/libc/socketpair-close-while-blocked.stderr index 97b5df7fb17ff..a7c660e1adcc3 100644 --- a/src/tools/miri/tests/fail-dep/libc/socketpair-close-while-blocked.stderr +++ b/src/tools/miri/tests/fail-dep/libc/socketpair-close-while-blocked.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -18,7 +18,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/libc/socketpair-close-while-blocked.rs:LL:CC | LL | libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) - | ^ this thread got stuck here + | ^ thread `unnamed-ID` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/libc/socketpair_block_read_twice.stderr b/src/tools/miri/tests/fail-dep/libc/socketpair_block_read_twice.stderr index 38db735e9b4d4..faab75f7840b6 100644 --- a/src/tools/miri/tests/fail-dep/libc/socketpair_block_read_twice.stderr +++ b/src/tools/miri/tests/fail-dep/libc/socketpair_block_read_twice.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -18,7 +18,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/libc/socketpair_block_read_twice.rs:LL:CC | LL | libc::read(fds[1], buf.as_mut_ptr().cast(), buf.len() as libc::size_t) - | ^ this thread got stuck here + | ^ thread `unnamed-ID` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail-dep/libc/socketpair_block_write_twice.stderr b/src/tools/miri/tests/fail-dep/libc/socketpair_block_write_twice.stderr index a2f1c67b5efc8..9f95d98beb6f0 100644 --- a/src/tools/miri/tests/fail-dep/libc/socketpair_block_write_twice.stderr +++ b/src/tools/miri/tests/fail-dep/libc/socketpair_block_write_twice.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC | LL | let ret = unsafe { libc::pthread_join(id, ptr::null_mut()) }; - | ^ this thread got stuck here + | ^ thread `main` got stuck here | = note: BACKTRACE: = note: inside `std::sys::thread::PLATFORM::Thread::join` at RUSTLIB/std/src/sys/thread/PLATFORM.rs:LL:CC @@ -18,7 +18,7 @@ error: the evaluated program deadlocked --> tests/fail-dep/libc/socketpair_block_write_twice.rs:LL:CC | LL | let res = unsafe { libc::write(fds[0], data.as_ptr() as *const libc::c_void, data.len()) }; - | ^ this thread got stuck here + | ^ thread `unnamed-ID` got stuck here note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace diff --git a/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.rs b/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.rs index b996fcaf45df1..9c73f6c03edd4 100644 --- a/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.rs +++ b/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.rs @@ -3,6 +3,9 @@ //@normalize-stderr-test: "LL \| .*" -> "LL | $$CODE" //@normalize-stderr-test: "\| +\^+" -> "| ^" //@normalize-stderr-test: "\n *= note:.*" -> "" +// On macOS we use chekced pthread mutexes which changes the error +//@normalize-stderr-test: "this thread got stuck here" -> "thread `main` got stuck here" +//@normalize-stderr-test: "a thread deadlocked" -> "the evaluated program deadlocked" use std::mem; use std::sync::Mutex; diff --git a/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.stderr b/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.stderr index cc487c62d08d2..7784132a54ce8 100644 --- a/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.stderr +++ b/src/tools/miri/tests/fail/concurrency/mutex-leak-move-deadlock.stderr @@ -2,7 +2,7 @@ error: the evaluated program deadlocked --> RUSTLIB/std/$FILE:LL:CC | LL | $CODE - | ^ this thread got stuck here + | ^ thread `main` got stuck here | note: inside `main` --> tests/fail/concurrency/mutex-leak-move-deadlock.rs:LL:CC diff --git a/src/tools/miri/tests/genmc/fail/shims/mutex_diff_thread_unlock.stderr b/src/tools/miri/tests/genmc/fail/shims/mutex_diff_thread_unlock.stderr index e2148bedd3187..db465969cda81 100644 --- a/src/tools/miri/tests/genmc/fail/shims/mutex_diff_thread_unlock.stderr +++ b/src/tools/miri/tests/genmc/fail/shims/mutex_diff_thread_unlock.stderr @@ -1,64 +1,4 @@ Running GenMC Verification... -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - = note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC - = note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC - = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC - = note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC - = note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `miri_start` - --> tests/genmc/fail/shims/mutex_diff_thread_unlock.rs:LL:CC - | -LL | let handle = std::thread::spawn(move || { - | __________________^ -LL | | let guard = guard; // avoid field capturing -LL | | drop(guard); -LL | | }); - | |______^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - = note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC - = note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC - = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC - = note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC - = note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `miri_start` - --> tests/genmc/fail/shims/mutex_diff_thread_unlock.rs:LL:CC - | -LL | let handle = std::thread::spawn(move || { - | __________________^ -LL | | let guard = guard; // avoid field capturing -LL | | drop(guard); -LL | | }); - | |______^ - error: Undefined Behavior: Invalid unlock() operation --> RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC | @@ -82,5 +22,5 @@ note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report -error: aborting due to 1 previous error; 2 warnings emitted +error: aborting due to 1 previous error diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs index e32c7cdf80c43..c19c81995d1bc 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs +++ b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs @@ -30,5 +30,10 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize { if 2 != VALUE.load(SeqCst) { std::process::abort() } + + // Check that we emit warnings for cases that are not fully supported. + let _ = VALUE.compare_exchange(99, 99, SeqCst, Relaxed); + let _ = VALUE.compare_exchange_weak(99, 99, Relaxed, SeqCst); + 0 } diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr index 7867be2dbe8ed..4351b312c75dc 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr +++ b/src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr @@ -1,2 +1,20 @@ Running GenMC Verification... +warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'SeqCst', the failure ordering 'Relaxed' is treated like 'SeqCst'. Miri with GenMC might miss bugs related to this memory access. + --> tests/genmc/pass/atomics/cas_simple.rs:LL:CC + | +LL | let _ = VALUE.compare_exchange(99, 99, SeqCst, Relaxed); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + +warning: GenMC currently does not model the failure ordering for `compare_exchange`. Success ordering 'Relaxed' was upgraded to 'SeqCst' to match failure ordering 'SeqCst'. Miri with GenMC might miss bugs related to this memory access. + --> tests/genmc/pass/atomics/cas_simple.rs:LL:CC + | +LL | let _ = VALUE.compare_exchange_weak(99, 99, Relaxed, SeqCst); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + +warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. + --> tests/genmc/pass/atomics/cas_simple.rs:LL:CC + | +LL | let _ = VALUE.compare_exchange_weak(99, 99, Relaxed, SeqCst); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + Verification complete with 1 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr b/src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr index fdbb9eff2faa6..a67635dee1bef 100644 --- a/src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr +++ b/src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr @@ -1,126 +1,2 @@ Running GenMC Verification... -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/thread/id.rs:LL:CC - | -LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let weak = Arc::downgrade(&data_clone); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let weak = Arc::downgrade(&data_clone); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let handle = std::thread::spawn(move || { - | __________________^ -... | -LL | | }); - | |______^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let handle = std::thread::spawn(move || { - | __________________^ -... | -LL | | }); - | |______^ - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | handle.join().unwrap(); - | ^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/rt.rs:LL:CC - | -LL | / CLEANUP.call_once(|| unsafe { -LL | | // Flush stdout and disable buffering. -LL | | crate::io::cleanup(); -... | -LL | | }); - | |______^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sync/once.rs:LL:CC - | -LL | self.inner.call(true, &mut |p| f.take().unwrap()(p)); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC - | -LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - Verification complete with 4 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/std/arc.rs b/src/tools/miri/tests/genmc/pass/std/arc.rs index dee29127856df..addf6408c006f 100644 --- a/src/tools/miri/tests/genmc/pass/std/arc.rs +++ b/src/tools/miri/tests/genmc/pass/std/arc.rs @@ -1,6 +1,5 @@ //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows //@revisions: check_count try_upgrade -//@normalize-stderr-test: "\n *= note: inside `std::.*" -> "" // Check that various operations on `std::sync::Arc` are handled properly in GenMC mode. // diff --git a/src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr b/src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr index a5423f9a398bb..f527b61202327 100644 --- a/src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr +++ b/src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr @@ -1,152 +1,2 @@ Running GenMC Verification... -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/thread/id.rs:LL:CC - | -LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let weak = Arc::downgrade(&data_clone); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let weak = Arc::downgrade(&data_clone); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let handle = std::thread::spawn(move || { - | __________________^ -... | -LL | | }); - | |______^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | let handle = std::thread::spawn(move || { - | __________________^ -... | -LL | | }); - | |______^ - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside `main` - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | handle.join().unwrap(); - | ^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/rt.rs:LL:CC - | -LL | / CLEANUP.call_once(|| unsafe { -LL | | // Flush stdout and disable buffering. -LL | | crate::io::cleanup(); -... | -LL | | }); - | |______^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sync/once.rs:LL:CC - | -LL | self.inner.call(true, &mut |p| f.take().unwrap()(p)); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC - | -LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | if self.inner()?.strong.fetch_update(Acquire, Relaxed, checked_increment).is_ok() { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE on thread `unnamed-ID`: -note: inside closure - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | if let Some(strong) = weak_.upgrade() { - | ^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | if self.inner()?.strong.fetch_update(Acquire, Relaxed, checked_increment).is_ok() { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE on thread `unnamed-ID`: -note: inside closure - --> tests/genmc/pass/std/arc.rs:LL:CC - | -LL | if let Some(strong) = weak_.upgrade() { - | ^^^^^^^^^^^^^^^ - Verification complete with 7 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/std/empty_main.rs b/src/tools/miri/tests/genmc/pass/std/empty_main.rs index f0e4155ccd5dd..2ffc3388fb36c 100644 --- a/src/tools/miri/tests/genmc/pass/std/empty_main.rs +++ b/src/tools/miri/tests/genmc/pass/std/empty_main.rs @@ -1,5 +1,4 @@ //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -//@normalize-stderr-test: "\n *= note: inside `std::.*" -> "" // A lot of code runs before main, which we should be able to handle in GenMC mode. diff --git a/src/tools/miri/tests/genmc/pass/std/empty_main.stderr b/src/tools/miri/tests/genmc/pass/std/empty_main.stderr index de07943b0d8d1..7867be2dbe8ed 100644 --- a/src/tools/miri/tests/genmc/pass/std/empty_main.stderr +++ b/src/tools/miri/tests/genmc/pass/std/empty_main.stderr @@ -1,45 +1,2 @@ Running GenMC Verification... -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/thread/id.rs:LL:CC - | -LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/rt.rs:LL:CC - | -LL | / CLEANUP.call_once(|| unsafe { -LL | | // Flush stdout and disable buffering. -LL | | crate::io::cleanup(); -... | -LL | | }); - | |______^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sync/once.rs:LL:CC - | -LL | self.inner.call(true, &mut |p| f.take().unwrap()(p)); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC - | -LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - Verification complete with 1 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs index e32979dc2b510..dadbee47b9860 100644 --- a/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs +++ b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs @@ -1,5 +1,4 @@ //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -//@normalize-stderr-test: "\n *= note: inside `std::.*" -> "" // We should be able to spawn and join standard library threads in GenMC mode. // Since these threads do nothing, we should only explore 1 program execution. diff --git a/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr index 701934a7cd7f1..7867be2dbe8ed 100644 --- a/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr +++ b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr @@ -1,130 +1,2 @@ Running GenMC Verification... -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/thread/id.rs:LL:CC - | -LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside closure - --> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC - | -LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect(); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - = note: inside closure at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC - = note: inside ` as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC - = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC - = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec>::extend_trusted, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC - = note: inside `> as std::vec::spec_extend::SpecExtend, std::iter::Map, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::spec_extend` at RUSTLIB/alloc/src/vec/spec_extend.rs:LL:CC - = note: inside `> as std::vec::spec_from_iter_nested::SpecFromIterNested, std::iter::Map, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter_nested.rs:LL:CC - = note: inside `> as std::vec::spec_from_iter::SpecFromIter, std::iter::Map, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter.rs:LL:CC - = note: inside `> as std::iter::FromIterator>>::from_iter::, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC - = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::>>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC - | -LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect(); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside closure - --> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC - | -LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect(); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - = note: inside closure at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC - = note: inside ` as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC - = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC - = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec>::extend_trusted, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC - = note: inside `> as std::vec::spec_extend::SpecExtend, std::iter::Map, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::spec_extend` at RUSTLIB/alloc/src/vec/spec_extend.rs:LL:CC - = note: inside `> as std::vec::spec_from_iter_nested::SpecFromIterNested, std::iter::Map, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter_nested.rs:LL:CC - = note: inside `> as std::vec::spec_from_iter::SpecFromIter, std::iter::Map, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter.rs:LL:CC - = note: inside `> as std::iter::FromIterator>>::from_iter::, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC - = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::>>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC - | -LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect(); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside closure - --> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC - | -LL | handles.into_iter().for_each(|handle| handle.join().unwrap()); - | ^^^^^^^^^^^^^ - = note: inside closure at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC - = note: inside `> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/alloc/src/vec/into_iter.rs:LL:CC - = note: inside `> as std::iter::Iterator>::for_each::<{closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC - | -LL | handles.into_iter().for_each(|handle| handle.join().unwrap()); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/rt.rs:LL:CC - | -LL | / CLEANUP.call_once(|| unsafe { -LL | | // Flush stdout and disable buffering. -LL | | crate::io::cleanup(); -... | -LL | | }); - | |______^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sync/once.rs:LL:CC - | -LL | self.inner.call(true, &mut |p| f.take().unwrap()(p)); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC - | -LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - Verification complete with 1 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/std/thread_locals.rs b/src/tools/miri/tests/genmc/pass/std/thread_locals.rs index 4dac775d34070..d76975d2e92c2 100644 --- a/src/tools/miri/tests/genmc/pass/std/thread_locals.rs +++ b/src/tools/miri/tests/genmc/pass/std/thread_locals.rs @@ -1,5 +1,4 @@ //@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc -Zmiri-disable-stacked-borrows -//@normalize-stderr-test: "\n *= note: inside `std::.*" -> "" use std::alloc::{Layout, alloc}; use std::cell::Cell; diff --git a/src/tools/miri/tests/genmc/pass/std/thread_locals.stderr b/src/tools/miri/tests/genmc/pass/std/thread_locals.stderr index fd6538fd70faa..bde951866d013 100644 --- a/src/tools/miri/tests/genmc/pass/std/thread_locals.stderr +++ b/src/tools/miri/tests/genmc/pass/std/thread_locals.stderr @@ -1,113 +1,2 @@ Running GenMC Verification... -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/thread/id.rs:LL:CC - | -LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/thread_locals.rs:LL:CC - | -LL | / std::thread::spawn(|| { -LL | | R.set(unsafe { malloc() }); -LL | | let r_ptr = R.get(); -LL | | let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst); -LL | | }), - | |__________^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC - | -LL | || self - | ________________^ -LL | | .state -LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed) - | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/thread/lifecycle.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/thread_locals.rs:LL:CC - | -LL | / std::thread::spawn(|| { -LL | | R.set(unsafe { malloc() }); -LL | | let r_ptr = R.get(); -LL | | let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst); -LL | | }), - | |__________^ - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/alloc/src/sync.rs:LL:CC - | -LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: -note: inside closure - --> tests/genmc/pass/std/thread_locals.rs:LL:CC - | -LL | handles.into_iter().for_each(|handle| handle.join().unwrap()); - | ^^^^^^^^^^^^^ - = note: inside closure at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC - = note: inside closure at RUSTLIB/core/src/ops/try_trait.rs:LL:CC - = note: inside closure at RUSTLIB/core/src/array/iter/iter_inner.rs:LL:CC - = note: inside `::try_fold::<(), {closure@std::array::iter::iter_inner::PolymorphicIter<[std::mem::MaybeUninit>]>::try_fold<(), {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_2<(), std::thread::JoinHandle<()>, {closure@std::iter::Iterator::for_each::call, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>::{closure#0}}, std::ops::try_trait::NeverShortCircuit<()>>::{closure#0}}, std::ops::try_trait::NeverShortCircuit<()>>` at RUSTLIB/core/src/ops/index_range.rs:LL:CC - = note: inside `, 3> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/core/src/array/iter.rs:LL:CC - = note: inside `, 3> as std::iter::Iterator>::for_each::<{closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC -note: inside `main` - --> tests/genmc/pass/std/thread_locals.rs:LL:CC - | -LL | handles.into_iter().for_each(|handle| handle.join().unwrap()); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/rt.rs:LL:CC - | -LL | / CLEANUP.call_once(|| unsafe { -LL | | // Flush stdout and disable buffering. -LL | | crate::io::cleanup(); -... | -LL | | }); - | |______^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures. - --> RUSTLIB/std/src/sync/once.rs:LL:CC - | -LL | self.inner.call(true, &mut |p| f.take().unwrap()(p)); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/sync/once.rs:LL:CC - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - -warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access. - --> RUSTLIB/std/src/sys/exit_guard.rs:LL:CC - | -LL | match EXITING_THREAD_ID.compare_exchange(ptr::null_mut(), this_thread_id, Acquire, Relaxed) { - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code - | - = note: BACKTRACE: - = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC - Verification complete with 2 executions. No errors found. diff --git a/src/tools/miri/tests/pass/ptr_int_casts.rs b/src/tools/miri/tests/pass/ptr_int_casts.rs index 94391eac3b274..2d99a8a449b32 100644 --- a/src/tools/miri/tests/pass/ptr_int_casts.rs +++ b/src/tools/miri/tests/pass/ptr_int_casts.rs @@ -1,4 +1,6 @@ //@compile-flags: -Zmiri-permissive-provenance +//@revisions: stack tree +//@[tree]compile-flags: -Zmiri-tree-borrows use std::{mem, ptr}; fn eq_ref(x: &T, y: &T) -> bool { diff --git a/src/tools/miri/tests/pass/ptr_int_casts.tree.stderr b/src/tools/miri/tests/pass/ptr_int_casts.tree.stderr deleted file mode 100644 index 21c5b2b0dfe8f..0000000000000 --- a/src/tools/miri/tests/pass/ptr_int_casts.tree.stderr +++ /dev/null @@ -1,89 +0,0 @@ -warning: integer-to-pointer cast - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | assert_eq!(1 as *const i32 as usize, 1); - | ^^^^^^^^^^^^^^^ integer-to-pointer cast - | - = help: this program is using integer-to-pointer casts or (equivalently) `ptr::with_exposed_provenance`, which means that Miri might miss pointer bugs in this program - = help: see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation - = help: to ensure that Miri does not miss bugs in your program, use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead - = help: you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics - = help: Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used - = note: BACKTRACE: - = note: inside `ptr_int_casts` at tests/pass/ptr_int_casts.rs:LL:CC -note: inside `main` - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | ptr_int_casts(); - | ^^^^^^^^^^^^^^^ - -warning: integer-to-pointer cast - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | assert_eq!((1 as *const i32).wrapping_offset(4) as usize, 1 + 4 * 4); - | ^^^^^^^^^^^^^^^^^ integer-to-pointer cast - | - = note: BACKTRACE: - = note: inside `ptr_int_casts` at tests/pass/ptr_int_casts.rs:LL:CC -note: inside `main` - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | ptr_int_casts(); - | ^^^^^^^^^^^^^^^ - -warning: integer-to-pointer cast - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | *val = (1 as *const u8).wrapping_offset(-4); - | ^^^^^^^^^^^^^^^^ integer-to-pointer cast - | - = note: BACKTRACE: - = note: inside `ptr_int_casts` at tests/pass/ptr_int_casts.rs:LL:CC -note: inside `main` - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | ptr_int_casts(); - | ^^^^^^^^^^^^^^^ - -warning: integer-to-pointer cast - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | let y = y as *const _; - | ^^^^^^^^^^^^^ integer-to-pointer cast - | - = note: BACKTRACE: - = note: inside `ptr_int_casts` at tests/pass/ptr_int_casts.rs:LL:CC -note: inside `main` - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | ptr_int_casts(); - | ^^^^^^^^^^^^^^^ - -warning: integer-to-pointer cast - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | let x: fn() -> i32 = unsafe { mem::transmute(y as *mut u8) }; - | ^^^^^^^^^^^^ integer-to-pointer cast - | - = note: BACKTRACE: - = note: inside `ptr_int_casts` at tests/pass/ptr_int_casts.rs:LL:CC -note: inside `main` - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | ptr_int_casts(); - | ^^^^^^^^^^^^^^^ - -warning: integer-to-pointer cast - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | assert_eq!((-1i32) as usize as *const i32 as usize, (-1i32) as usize); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ integer-to-pointer cast - | - = note: BACKTRACE: - = note: inside `ptr_int_casts` at tests/pass/ptr_int_casts.rs:LL:CC -note: inside `main` - --> tests/pass/ptr_int_casts.rs:LL:CC - | -LL | ptr_int_casts(); - | ^^^^^^^^^^^^^^^ - 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 98f8f15608e1d..200e4b2ea3e94 100644 --- a/src/tools/miri/tests/pass/ptr_int_from_exposed.rs +++ b/src/tools/miri/tests/pass/ptr_int_from_exposed.rs @@ -1,4 +1,6 @@ //@compile-flags: -Zmiri-permissive-provenance +//@revisions: stack tree +//@[tree]compile-flags: -Zmiri-tree-borrows use std::ptr; diff --git a/src/tools/miri/tests/pass/ptr_int_from_exposed.tree.stderr b/src/tools/miri/tests/pass/ptr_int_from_exposed.tree.stderr deleted file mode 100644 index aac6d0f48d015..0000000000000 --- a/src/tools/miri/tests/pass/ptr_int_from_exposed.tree.stderr +++ /dev/null @@ -1,19 +0,0 @@ -warning: integer-to-pointer cast - --> tests/pass/ptr_int_from_exposed.rs:LL:CC - | -LL | let ptr = ptr::with_exposed_provenance::(x_usize).wrapping_offset(-128); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ integer-to-pointer cast - | - = help: this program is using integer-to-pointer casts or (equivalently) `ptr::with_exposed_provenance`, which means that Miri might miss pointer bugs in this program - = help: see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation - = help: to ensure that Miri does not miss bugs in your program, use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead - = help: you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics - = help: Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used - = note: BACKTRACE: - = note: inside `ptr_roundtrip_out_of_bounds` at tests/pass/ptr_int_from_exposed.rs:LL:CC -note: inside `main` - --> tests/pass/ptr_int_from_exposed.rs:LL:CC - | -LL | ptr_roundtrip_out_of_bounds(); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - diff --git a/src/tools/miri/triagebot.toml b/src/tools/miri/triagebot.toml index 060b749676e62..57c8f5782e0a5 100644 --- a/src/tools/miri/triagebot.toml +++ b/src/tools/miri/triagebot.toml @@ -53,9 +53,6 @@ new_draft = true # Canonicalize issue numbers to avoid closing the wrong issue when upstreaming this subtree. [canonicalize-issue-links] -# Prevents mentions in commits to avoid users being spammed. -[no-mentions] - # Show range-diff links on force pushes. [range-diff]