user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Rollup merge of #148523 - RalfJung:miri, r=RalfJung

Browse source 
miri subtree update

x86/rounding-error is causing spurious test failures. This sync fixes that.

---

Subtree update of `miri` to de2a63b1e2.

Created using https://github.com/rust-lang/josh-sync.

r? ``@ghost``
This commit is contained in:
Matthias Krüger 2025-11-05 21:28:30 +01:00 • committed by GitHub
commit 5ed4fafff2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
27 changed files with 277 additions and 304 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/tools/miri/README.md
View file

@ -220,7 +220,6 @@ degree documented below):
- `solaris` / `illumos`: maintained by @devnexen. Supports the entire test suite.
- `freebsd`: maintained by @YohDeadfall and @LorrensP-2158466. Supports the entire test suite.
- `android`: **maintainer wanted**. Support very incomplete, but a basic "hello world" works.
- `wasi`: **maintainer wanted**. Support very incomplete, but a basic "hello world" works.
- For targets on other operating systems, Miri might fail before even reaching the `main` function.
However, even for targets that we do support, the degree of support for accessing platform APIs

1
src/tools/miri/ci/ci.sh
View file

@ -153,7 +153,6 @@ case $HOST_TARGET in
BASIC="empty_main integer heap_alloc libc-mem vec string btreemap" # ensures we have the basics: pre-main code, system allocator
UNIX="hello panic/panic panic/unwind concurrency/simple atomic libc-mem libc-misc libc-random env num_cpus" # the things that are very similar across all Unixes, and hence easily supported there
TEST_TARGET=aarch64-linux-android run_tests_minimal $BASIC $UNIX time hashmap random thread sync concurrency epoll eventfd
TEST_TARGET=wasm32-wasip2 run_tests_minimal $BASIC hello wasm
TEST_TARGET=wasm32-unknown-unknown run_tests_minimal no_std empty_main wasm # this target doesn't really have std
TEST_TARGET=thumbv7em-none-eabihf run_tests_minimal no_std
;;

4
src/tools/miri/genmc-sys/build.rs
View file

@ -26,9 +26,9 @@ mod downloading {
use super::GENMC_DOWNLOAD_PATH;
/// The GenMC repository the we get our commit from.
pub(crate) const GENMC_GITHUB_URL: &str = "https://gitlab.inf.ethz.ch/public-plf/genmc.git";
pub(crate) const GENMC_GITHUB_URL: &str = "https://github.com/MPI-SWS/genmc.git";
/// The GenMC commit we depend on. It must be available on the specified GenMC repository.
pub(crate) const GENMC_COMMIT: &str = "ce775ccd7866db820fa12ffca66463087a11dd96";
pub(crate) const GENMC_COMMIT: &str = "d9527280bb99f1cef64326b1803ffd952e3880df";
/// Ensure that a local GenMC repo is present and set to the correct commit.
/// Return the path of the GenMC repo and whether the checked out commit was changed.

8
src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
View file

@ -261,7 +261,7 @@ namespace GenmcScalarExt {
inline GenmcScalar uninit() {
return GenmcScalar {
.value = 0,
.extra = 0,
.provenance = 0,
.is_init = false,
};
}
@ -269,19 +269,19 @@ inline GenmcScalar uninit() {
inline GenmcScalar from_sval(SVal sval) {
return GenmcScalar {
.value = sval.get(),
.extra = sval.getExtra(),
.provenance = sval.getProvenance(),
.is_init = true,
};
}
inline SVal to_sval(GenmcScalar scalar) {
ERROR_ON(!scalar.is_init, "Cannot convert an uninitialized `GenmcScalar` into an `SVal`\n");
return SVal(scalar.value, scalar.extra);
return SVal(scalar.value, scalar.provenance);
}
inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
if (scalar.is_init)
return { SVal(scalar.value, scalar.extra) };
return { SVal(scalar.value, scalar.provenance) };
return std::nullopt;
}
} // namespace GenmcScalarExt

11
src/tools/miri/genmc-sys/src/lib.rs
View file

@ -45,14 +45,14 @@ pub fn create_genmc_driver_handle(
}
impl GenmcScalar {
pub const UNINIT: Self = Self { value: 0, extra: 0, is_init: false };
pub const UNINIT: Self = Self { value: 0, provenance: 0, is_init: false };
pub const fn from_u64(value: u64) -> Self {
Self { value, extra: 0, is_init: true }
Self { value, provenance: 0, is_init: true }
}
pub const fn has_provenance(&self) -> bool {
self.extra != 0
self.provenance != 0
}
}
@ -172,8 +172,9 @@ mod ffi {
value: u64,
/// This is zero for integer values. For pointers, this encodes the provenance by
/// storing the base address of the allocation that this pointer belongs to.
/// Operations on `SVal` in GenMC (e.g., `fetch_add`) preserve the `extra` of the left argument (`left.fetch_add(right, ...)`).
extra: u64,
/// Operations on `SVal` in GenMC (e.g., `fetch_add`) preserve the `provenance` of the left
/// argument (`left.fetch_add(right, ...)`).
provenance: u64,
/// Indicates whether this value is initialized. If this is `false`, the other fields do not matter.
/// (Ideally we'd use `std::optional` but CXX does not support that.)
is_init: bool,

2
src/tools/miri/rust-version
View file

@ -1 +1 @@
292be5c7c05138d753bbd4b30db7a3f1a5c914f7
5f9dd05862d2e4bceb3be1031b6c936e35671501

8
src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
View file

@ -640,7 +640,7 @@ mod propagation_optimization_checks {
impl Exhaustive for AccessRelatedness {
fn exhaustive() -> Box<dyn Iterator<Item = Self>> {
use AccessRelatedness::*;
Box::new(vec![This, StrictChildAccess, AncestorAccess, CousinAccess].into_iter())
Box::new(vec![ForeignAccess, LocalAccess].into_iter())
}
}
@ -716,13 +716,11 @@ mod propagation_optimization_checks {
// We now assert it is idempotent, and never causes UB.
// First, if the SIFA includes foreign reads, assert it is idempotent under foreign reads.
if access >= IdempotentForeignAccess::Read {
// We use `CousinAccess` here. We could also use `AncestorAccess`, since `transition::perform_access` treats these the same.
// The only place they are treated differently is in protector end accesses, but these are not handled here.
assert_eq!(perm, transition::perform_access(AccessKind::Read, AccessRelatedness::CousinAccess, perm, prot).unwrap());
assert_eq!(perm, transition::perform_access(AccessKind::Read, AccessRelatedness::ForeignAccess, perm, prot).unwrap());
}
// Then, if the SIFA includes foreign writes, assert it is idempotent under foreign writes.
if access >= IdempotentForeignAccess::Write {
assert_eq!(perm, transition::perform_access(AccessKind::Write, AccessRelatedness::CousinAccess, perm, prot).unwrap());
assert_eq!(perm, transition::perform_access(AccessKind::Write, AccessRelatedness::ForeignAccess, perm, prot).unwrap());
}
}
}

75
src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs
View file

@ -24,7 +24,7 @@ use crate::borrow_tracker::tree_borrows::diagnostics::{
};
use crate::borrow_tracker::tree_borrows::foreign_access_skipping::IdempotentForeignAccess;
use crate::borrow_tracker::tree_borrows::perms::PermTransition;
use crate::borrow_tracker::tree_borrows::unimap::{UniEntry, UniIndex, UniKeyMap, UniValMap};
use crate::borrow_tracker::tree_borrows::unimap::{UniIndex, UniKeyMap, UniValMap};
use crate::borrow_tracker::{GlobalState, ProtectorKind};
use crate::*;
@ -265,13 +265,15 @@ pub(super) struct Node {
}
/// Data given to the transition function
struct NodeAppArgs<'node> {
/// Node on which the transition is currently being applied
node: &'node mut Node,
/// Mutable access to its permissions
perm: UniEntry<'node, LocationState>,
/// Relative position of the access
struct NodeAppArgs<'visit> {
/// The index of the current node.
idx: UniIndex,
/// Relative position of the access.
rel_pos: AccessRelatedness,
/// The node map of this tree.
nodes: &'visit mut UniValMap<Node>,
/// The permissions map of this tree.
perms: &'visit mut UniValMap<LocationState>,
}
/// Data given to the error handler
struct ErrHandlerArgs<'node, InErr> {
@ -348,8 +350,7 @@ where
idx: UniIndex,
rel_pos: AccessRelatedness,
) -> ContinueTraversal {
let node = this.nodes.get_mut(idx).unwrap();
let args = NodeAppArgs { node, perm: this.perms.entry(idx), rel_pos };
let args = NodeAppArgs { idx, rel_pos, nodes: this.nodes, perms: this.perms };
(self.f_continue)(&args)
}
@ -359,16 +360,14 @@ where
idx: UniIndex,
rel_pos: AccessRelatedness,
) -> Result<(), OutErr> {
let node = this.nodes.get_mut(idx).unwrap();
(self.f_propagate)(NodeAppArgs { node, perm: this.perms.entry(idx), rel_pos }).map_err(
|error_kind| {
(self.f_propagate)(NodeAppArgs { idx, rel_pos, nodes: this.nodes, perms: this.perms })
.map_err(|error_kind| {
(self.err_builder)(ErrHandlerArgs {
error_kind,
conflicting_info: &this.nodes.get(idx).unwrap().debug_info,
accessed_info: &this.nodes.get(self.initial).unwrap().debug_info,
})
},
)
})
}
fn go_upwards_from_accessed(
@ -386,14 +385,14 @@ where
// be handled differently here compared to the further parents
// of `accesssed_node`.
{
self.propagate_at(this, accessed_node, AccessRelatedness::This)?;
self.propagate_at(this, accessed_node, AccessRelatedness::LocalAccess)?;
if matches!(visit_children, ChildrenVisitMode::VisitChildrenOfAccessed) {
let accessed_node = this.nodes.get(accessed_node).unwrap();
// We `rev()` here because we reverse the entire stack later.
for &child in accessed_node.children.iter().rev() {
self.stack.push((
child,
AccessRelatedness::AncestorAccess,
AccessRelatedness::ForeignAccess,
RecursionState::BeforeChildren,
));
}
@ -404,7 +403,7 @@ where
// not the subtree that contains the accessed node.
let mut last_node = accessed_node;
while let Some(current) = this.nodes.get(last_node).unwrap().parent {
self.propagate_at(this, current, AccessRelatedness::StrictChildAccess)?;
self.propagate_at(this, current, AccessRelatedness::LocalAccess)?;
let node = this.nodes.get(current).unwrap();
// We `rev()` here because we reverse the entire stack later.
for &child in node.children.iter().rev() {
@ -413,7 +412,7 @@ where
}
self.stack.push((
child,
AccessRelatedness::CousinAccess,
AccessRelatedness::ForeignAccess,
RecursionState::BeforeChildren,
));
}
@ -741,7 +740,9 @@ impl<'tcx> Tree {
// visit all children, skipping none
|_| ContinueTraversal::Recurse,
|args: NodeAppArgs<'_>| -> Result<(), TransitionError> {
let NodeAppArgs { node, perm, .. } = args;
let node = args.nodes.get(args.idx).unwrap();
let perm = args.perms.entry(args.idx);
let perm =
perm.get().copied().unwrap_or_else(|| node.default_location_state());
if global.borrow().protected_tags.get(&node.tag)
@ -812,32 +813,34 @@ impl<'tcx> Tree {
// `perms_range` is only for diagnostics (it is the range of
// the `RangeMap` on which we are currently working).
let node_skipper = |access_kind: AccessKind, args: &NodeAppArgs<'_>| -> ContinueTraversal {
let NodeAppArgs { node, perm, rel_pos } = args;
let node = args.nodes.get(args.idx).unwrap();
let perm = args.perms.get(args.idx);
let old_state = perm.get().copied().unwrap_or_else(|| node.default_location_state());
old_state.skip_if_known_noop(access_kind, *rel_pos)
let old_state = perm.copied().unwrap_or_else(|| node.default_location_state());
old_state.skip_if_known_noop(access_kind, args.rel_pos)
};
let node_app = |perms_range: Range<u64>,
access_kind: AccessKind,
access_cause: diagnostics::AccessCause,
args: NodeAppArgs<'_>|
-> Result<(), TransitionError> {
let NodeAppArgs { node, mut perm, rel_pos } = args;
let node = args.nodes.get_mut(args.idx).unwrap();
let mut perm = args.perms.entry(args.idx);
let old_state = perm.or_insert(node.default_location_state());
// Call this function now, which ensures it is only called when
// `skip_if_known_noop` returns `Recurse`, due to the contract of
// `traverse_this_parents_children_other`.
old_state.record_new_access(access_kind, rel_pos);
old_state.record_new_access(access_kind, args.rel_pos);
let protected = global.borrow().protected_tags.contains_key(&node.tag);
let transition = old_state.perform_access(access_kind, rel_pos, protected)?;
let transition = old_state.perform_access(access_kind, args.rel_pos, protected)?;
// Record the event as part of the history
if !transition.is_noop() {
node.debug_info.history.push(diagnostics::Event {
transition,
is_foreign: rel_pos.is_foreign(),
is_foreign: args.rel_pos.is_foreign(),
access_cause,
access_range: access_range_and_kind.map(|x| x.0),
transition_range: perms_range,
@ -1075,24 +1078,18 @@ impl VisitProvenance for Tree {
/// Relative position of the access
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum AccessRelatedness {
/// The accessed pointer is the current one
This,
/// The accessed pointer is a (transitive) child of the current one.
// Current pointer is excluded (unlike in some other places of this module
// where "child" is inclusive).
StrictChildAccess,
/// The accessed pointer is a (transitive) parent of the current one.
// Current pointer is excluded.
AncestorAccess,
/// The accessed pointer is neither of the above.
// It's a cousin/uncle/etc., something in a side branch.
CousinAccess,
/// The access happened either through the node itself or one of
/// its transitive children.
LocalAccess,
/// The access happened through this nodes ancestor or through
/// a sibling/cousin/uncle/etc.
ForeignAccess,
}
impl AccessRelatedness {
/// Check that access is either Ancestor or Distant, i.e. not
/// a transitive child (initial pointer included).
pub fn is_foreign(self) -> bool {
matches!(self, AccessRelatedness::AncestorAccess | AccessRelatedness::CousinAccess)
matches!(self, AccessRelatedness::ForeignAccess)
}
}

12
src/tools/miri/src/borrow_tracker/tree_borrows/tree/tests.rs
View file

@ -263,15 +263,15 @@ mod spurious_read {
match xy_rel {
RelPosXY::MutuallyForeign =>
match self {
PtrSelector::X => (This, CousinAccess),
PtrSelector::Y => (CousinAccess, This),
PtrSelector::Other => (CousinAccess, CousinAccess),
PtrSelector::X => (LocalAccess, ForeignAccess),
PtrSelector::Y => (ForeignAccess, LocalAccess),
PtrSelector::Other => (ForeignAccess, ForeignAccess),
},
RelPosXY::XChildY =>
match self {
PtrSelector::X => (This, StrictChildAccess),
PtrSelector::Y => (AncestorAccess, This),
PtrSelector::Other => (CousinAccess, CousinAccess),
PtrSelector::X => (LocalAccess, LocalAccess),
PtrSelector::Y => (ForeignAccess, LocalAccess),
PtrSelector::Other => (ForeignAccess, ForeignAccess),
},
}
}

15
src/tools/miri/src/concurrency/genmc/helper.rs
View file

@ -55,7 +55,7 @@ pub fn scalar_to_genmc_scalar<'tcx>(
rustc_const_eval::interpret::Scalar::Int(scalar_int) => {
// FIXME(genmc): Add u128 support once GenMC supports it.
let value: u64 = scalar_int.to_uint(scalar_int.size()).try_into().unwrap();
GenmcScalar { value, extra: 0, is_init: true }
GenmcScalar { value, provenance: 0, is_init: true }
}
rustc_const_eval::interpret::Scalar::Ptr(pointer, size) => {
// FIXME(genmc,borrow tracking): Borrow tracking information is lost.
@ -69,7 +69,7 @@ pub fn scalar_to_genmc_scalar<'tcx>(
let base_addr = ecx.addr_from_alloc_id(alloc_id, None)?;
// Add the base_addr alloc_id pair to the map.
genmc_ctx.exec_state.genmc_shared_allocs_map.borrow_mut().insert(base_addr, alloc_id);
GenmcScalar { value: addr.bytes(), extra: base_addr, is_init: true }
GenmcScalar { value: addr.bytes(), provenance: base_addr, is_init: true }
}
})
}
@ -84,16 +84,17 @@ pub fn genmc_scalar_to_scalar<'tcx>(
scalar: GenmcScalar,
size: Size,
) -> InterpResult<'tcx, Scalar> {
// If `extra` is zero, we have a regular integer.
if scalar.extra == 0 {
// If `provenance` is zero, we have a regular integer.
if scalar.provenance == 0 {
// NOTE: GenMC always returns 64 bit values, and the upper bits are not yet truncated.
// FIXME(genmc): GenMC should be doing the truncation, not Miri.
let (value_scalar_int, _got_truncated) = ScalarInt::truncate_from_uint(scalar.value, size);
return interp_ok(Scalar::from(value_scalar_int));
}
// `extra` is non-zero, we have a pointer.
// When we get a pointer from GenMC, then we must have sent it to GenMC before in the same execution (since the reads-from relation is always respected).
let alloc_id = genmc_ctx.exec_state.genmc_shared_allocs_map.borrow()[&scalar.extra];
// `provenance` is non-zero, we have a pointer.
// When we get a pointer from GenMC, then we must have sent it to GenMC before in the same
// execution (since the reads-from relation is always respected).
let alloc_id = genmc_ctx.exec_state.genmc_shared_allocs_map.borrow()[&scalar.provenance];
// FIXME(genmc,borrow tracking): Borrow tracking not yet supported.
let provenance = machine::Provenance::Concrete { alloc_id, tag: BorTag::default() };
let ptr = interpret::Pointer::new(provenance, Size::from_bytes(scalar.value));

30
src/tools/miri/src/concurrency/thread.rs
View file

@ -181,7 +181,6 @@ pub struct Thread<'tcx> {
/// The index of the topmost user-relevant frame in `stack`. This field must contain
/// the value produced by `get_top_user_relevant_frame`.
/// The `None` state here represents
/// This field is a cache to reduce how often we call that method. The cache is manually
/// maintained inside `MiriMachine::after_stack_push` and `MiriMachine::after_stack_pop`.
top_user_relevant_frame: Option<usize>,
@ -232,12 +231,21 @@ impl<'tcx> Thread<'tcx> {
/// justifying the optimization that only pushes of user-relevant frames require updating the
/// `top_user_relevant_frame` field.
fn compute_top_user_relevant_frame(&self, skip: usize) -> Option<usize> {
self.stack
.iter()
.enumerate()
.rev()
.skip(skip)
.find_map(|(idx, frame)| if frame.extra.is_user_relevant { Some(idx) } else { None })
// We are search for the frame with maximum relevance.
let mut best = None;
for (idx, frame) in self.stack.iter().enumerate().rev().skip(skip) {
let relevance = frame.extra.user_relevance;
if relevance == u8::MAX {
// We can short-circuit this search.
return Some(idx);
}
if best.is_none_or(|(_best_idx, best_relevance)| best_relevance < relevance) {
// The previous best frame has strictly worse relevance, so despite us being lower
// in the stack, we win.
best = Some((idx, relevance));
}
}
best.map(|(idx, _relevance)| idx)
}
/// Re-compute the top user-relevant frame from scratch. `skip` indicates how many top frames
@ -256,14 +264,20 @@ impl<'tcx> Thread<'tcx> {
/// Returns the topmost frame that is considered user-relevant, or the
/// top of the stack if there is no such frame, or `None` if the stack is empty.
pub fn top_user_relevant_frame(&self) -> Option<usize> {
debug_assert_eq!(self.top_user_relevant_frame, self.compute_top_user_relevant_frame(0));
// This can be called upon creation of an allocation. We create allocations while setting up
// parts of the Rust runtime when we do not have any stack frames yet, so we need to handle
// empty stacks.
self.top_user_relevant_frame.or_else(|| self.stack.len().checked_sub(1))
}
pub fn current_user_relevance(&self) -> u8 {
self.top_user_relevant_frame()
.map(|frame_idx| self.stack[frame_idx].extra.user_relevance)
.unwrap_or(0)
}
pub fn current_user_relevant_span(&self) -> Span {
debug_assert_eq!(self.top_user_relevant_frame, self.compute_top_user_relevant_frame(0));
self.top_user_relevant_frame()
.map(|frame_idx| self.stack[frame_idx].current_span())
.unwrap_or(rustc_span::DUMMY_SP)

20
src/tools/miri/src/diagnostics.rs
View file

@ -187,16 +187,14 @@ pub fn prune_stacktrace<'tcx>(
}
BacktraceStyle::Short => {
let original_len = stacktrace.len();
// Only prune frames if there is at least one local frame. This check ensures that if
// we get a backtrace that never makes it to the user code because it has detected a
// bug in the Rust runtime, we don't prune away every frame.
let has_local_frame = stacktrace.iter().any(|frame| machine.is_local(frame));
// Remove all frames marked with `caller_location` -- that attribute indicates we
// usually want to point at the caller, not them.
stacktrace.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
// Only prune further frames if there is at least one local frame. This check ensures
// that if we get a backtrace that never makes it to the user code because it has
// detected a bug in the Rust runtime, we don't prune away every frame.
let has_local_frame = stacktrace.iter().any(|frame| machine.is_local(frame.instance));
if has_local_frame {
// Remove all frames marked with `caller_location` -- that attribute indicates we
// usually want to point at the caller, not them.
stacktrace
.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
// This is part of the logic that `std` uses to select the relevant part of a
// backtrace. But here, we only look for __rust_begin_short_backtrace, not
// __rust_end_short_backtrace because the end symbol comes from a call to the default
@ -216,7 +214,7 @@ pub fn prune_stacktrace<'tcx>(
// This len check ensures that we don't somehow remove every frame, as doing so breaks
// the primary error message.
while stacktrace.len() > 1
&& stacktrace.last().is_some_and(|frame| !machine.is_local(frame))
&& stacktrace.last().is_some_and(|frame| !machine.is_local(frame.instance))
{
stacktrace.pop();
}
@ -619,7 +617,7 @@ pub fn report_msg<'tcx>(
write!(backtrace_title, ":").unwrap();
err.note(backtrace_title);
for (idx, frame_info) in stacktrace.iter().enumerate() {
let is_local = machine.is_local(frame_info);
let is_local = machine.is_local(frame_info.instance);
// No span for non-local frames and the first frame (which is the error site).
if is_local && idx > 0 {
err.subdiagnostic(frame_info.as_note(machine.tcx));

17
src/tools/miri/src/helpers.rs
View file

@ -1088,11 +1088,18 @@ impl<'tcx> MiriMachine<'tcx> {
self.threads.active_thread_ref().top_user_relevant_frame()
}
/// This is the source of truth for the `is_user_relevant` flag in our `FrameExtra`.
pub fn is_user_relevant(&self, frame: &Frame<'tcx, Provenance>) -> bool {
let def_id = frame.instance().def_id();
(def_id.is_local() || self.user_relevant_crates.contains(&def_id.krate))
&& !frame.instance().def.requires_caller_location(self.tcx)
/// This is the source of truth for the `user_relevance` flag in our `FrameExtra`.
pub fn user_relevance(&self, frame: &Frame<'tcx, Provenance>) -> u8 {
if frame.instance().def.requires_caller_location(self.tcx) {
return 0;
}
if self.is_local(frame.instance()) {
u8::MAX
} else {
// A non-relevant frame, but at least it doesn't require a caller location, so
// better than nothing.
1
}
}
}

45
src/tools/miri/src/machine.rs
View file

@ -140,11 +140,10 @@ pub struct FrameExtra<'tcx> {
/// we use this to register a completed event with `measureme`.
pub timing: Option<measureme::DetachedTiming>,
/// Indicates whether a `Frame` is part of a workspace-local crate and is also not
/// `#[track_caller]`. We compute this once on creation and store the result, as an
/// optimization.
/// This is used by `MiriMachine::current_span` and `MiriMachine::caller_span`
pub is_user_relevant: bool,
/// Indicates how user-relevant this frame is. `#[track_caller]` frames are never relevant.
/// Frames from user-relevant crates are maximally relevant; frames from other crates are less
/// relevant.
pub user_relevance: u8,
/// Data race detector per-frame data.
pub data_race: Option<data_race::FrameState>,
@ -153,12 +152,12 @@ pub struct FrameExtra<'tcx> {
impl<'tcx> std::fmt::Debug for FrameExtra<'tcx> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
// Omitting `timing`, it does not support `Debug`.
let FrameExtra { borrow_tracker, catch_unwind, timing: _, is_user_relevant, data_race } =
let FrameExtra { borrow_tracker, catch_unwind, timing: _, user_relevance, data_race } =
self;
f.debug_struct("FrameData")
.field("borrow_tracker", borrow_tracker)
.field("catch_unwind", catch_unwind)
.field("is_user_relevant", is_user_relevant)
.field("user_relevance", user_relevance)
.field("data_race", data_race)
.finish()
}
@ -166,13 +165,8 @@ impl<'tcx> std::fmt::Debug for FrameExtra<'tcx> {
impl VisitProvenance for FrameExtra<'_> {
fn visit_provenance(&self, visit: &mut VisitWith<'_>) {
let FrameExtra {
catch_unwind,
borrow_tracker,
timing: _,
is_user_relevant: _,
data_race: _,
} = self;
let FrameExtra { catch_unwind, borrow_tracker, timing: _, user_relevance: _, data_race: _ } =
self;
catch_unwind.visit_provenance(visit);
borrow_tracker.visit_provenance(visit);
@ -911,8 +905,8 @@ impl<'tcx> MiriMachine<'tcx> {
}
/// Check whether the stack frame that this `FrameInfo` refers to is part of a local crate.
pub(crate) fn is_local(&self, frame: &FrameInfo<'_>) -> bool {
let def_id = frame.instance.def_id();
pub(crate) fn is_local(&self, instance: ty::Instance<'tcx>) -> bool {
let def_id = instance.def_id();
def_id.is_local() || self.user_relevant_crates.contains(&def_id.krate)
}
@ -1703,7 +1697,7 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
borrow_tracker: borrow_tracker.map(|bt| bt.borrow_mut().new_frame()),
catch_unwind: None,
timing,
is_user_relevant: ecx.machine.is_user_relevant(&frame),
user_relevance: ecx.machine.user_relevance(&frame),
data_race: ecx
.machine
.data_race
@ -1759,9 +1753,9 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
#[inline(always)]
fn after_stack_push(ecx: &mut InterpCx<'tcx, Self>) -> InterpResult<'tcx> {
if ecx.frame().extra.is_user_relevant {
// We just pushed a local frame, so we know that the topmost local frame is the topmost
// frame. If we push a non-local frame, there's no need to do anything.
if ecx.frame().extra.user_relevance >= ecx.active_thread_ref().current_user_relevance() {
// We just pushed a frame that's at least as relevant as the so-far most relevant frame.
// That means we are now the most relevant frame.
let stack_len = ecx.active_thread_stack().len();
ecx.active_thread_mut().set_top_user_relevant_frame(stack_len - 1);
}
@ -1775,9 +1769,14 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
if ecx.machine.borrow_tracker.is_some() {
ecx.on_stack_pop(frame)?;
}
if frame.extra.is_user_relevant {
// All that we store is whether or not the frame we just removed is local, so now we
// have no idea where the next topmost local frame is. So we recompute it.
if ecx
.active_thread_ref()
.top_user_relevant_frame()
.expect("there should always be a most relevant frame for a non-empty stack")
== ecx.frame_idx()
{
// We are popping the most relevant frame. We have no clue what the next relevant frame
// below that is, so we recompute that.
// (If this ever becomes a bottleneck, we could have `push` store the previous
// user-relevant frame and restore that here.)
// We have to skip the frame that is just being popped.

2
src/tools/miri/src/shims/env.rs
View file

@ -51,7 +51,7 @@ impl<'tcx> EnvVars<'tcx> {
} else if ecx.tcx.sess.target.os == "windows" {
EnvVars::Windows(WindowsEnvVars::new(ecx, env_vars)?)
} else {
// Used e.g. for wasi
// For "none" targets (i.e., without an OS).
EnvVars::Uninit
};
ecx.machine.env_vars = env_vars;

5
src/tools/miri/src/shims/foreign_items.rs
View file

@ -103,7 +103,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let this = self.eval_context_ref();
match this.tcx.sess.target.os.as_ref() {
os if this.target_os_is_unix() => shims::unix::foreign_items::is_dyn_sym(name, os),
"wasi" => shims::wasi::foreign_items::is_dyn_sym(name),
"windows" => shims::windows::foreign_items::is_dyn_sym(name),
_ => false,
}
@ -851,10 +850,6 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
shims::unix::foreign_items::EvalContextExt::emulate_foreign_item_inner(
this, link_name, abi, args, dest,
),
"wasi" =>
shims::wasi::foreign_items::EvalContextExt::emulate_foreign_item_inner(
this, link_name, abi, args, dest,
),
"windows" =>
shims::windows::foreign_items::EvalContextExt::emulate_foreign_item_inner(
this, link_name, abi, args, dest,

1
src/tools/miri/src/shims/mod.rs
View file

@ -8,7 +8,6 @@ mod math;
#[cfg(all(unix, feature = "native-lib"))]
mod native_lib;
mod unix;
mod wasi;
mod windows;
mod x86;

1
src/tools/miri/src/shims/tls.rs
View file

@ -253,7 +253,6 @@ impl<'tcx> TlsDtorsState<'tcx> {
}
_ => {
// No TLS dtor support.
// FIXME: should we do something on wasi?
break 'new_state Done;
}
}

110
src/tools/miri/src/shims/wasi/foreign_items.rs
View file

@ -1,110 +0,0 @@
use rustc_abi::CanonAbi;
use rustc_middle::ty::Ty;
use rustc_span::Symbol;
use rustc_target::callconv::FnAbi;
use crate::shims::alloc::EvalContextExt as _;
use crate::*;
pub fn is_dyn_sym(_name: &str) -> bool {
false
}
impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
fn emulate_foreign_item_inner(
&mut self,
link_name: Symbol,
abi: &FnAbi<'tcx, Ty<'tcx>>,
args: &[OpTy<'tcx>],
dest: &MPlaceTy<'tcx>,
) -> InterpResult<'tcx, EmulateItemResult> {
let this = self.eval_context_mut();
match link_name.as_str() {
// Allocation
"posix_memalign" => {
let [memptr, align, size] =
this.check_shim_sig_lenient(abi, CanonAbi::C, link_name, args)?;
let result = this.posix_memalign(memptr, align, size)?;
this.write_scalar(result, dest)?;
}
"aligned_alloc" => {
let [align, size] =
this.check_shim_sig_lenient(abi, CanonAbi::C, link_name, args)?;
let res = this.aligned_alloc(align, size)?;
this.write_pointer(res, dest)?;
}
// Standard input/output
// FIXME: These shims are hacks that just get basic stdout/stderr working. We can't
// constrain them to "std" since std itself uses the wasi crate for this.
"get-stdout" => {
let [] =
this.check_shim_sig(shim_sig!(extern "C" fn() -> i32), link_name, abi, args)?;
this.write_scalar(Scalar::from_i32(1), dest)?; // POSIX FD number for stdout
}
"get-stderr" => {
let [] =
this.check_shim_sig(shim_sig!(extern "C" fn() -> i32), link_name, abi, args)?;
this.write_scalar(Scalar::from_i32(2), dest)?; // POSIX FD number for stderr
}
"[resource-drop]output-stream" => {
let [handle] =
this.check_shim_sig(shim_sig!(extern "C" fn(i32) -> ()), link_name, abi, args)?;
let handle = this.read_scalar(handle)?.to_i32()?;
if !(handle == 1 || handle == 2) {
throw_unsup_format!("wasm output-stream: unsupported handle");
}
// We don't actually close these FDs, so this is a NOP.
}
"[method]output-stream.blocking-write-and-flush" => {
let [handle, buf, len, ret_area] = this.check_shim_sig(
shim_sig!(extern "C" fn(i32, *mut _, usize, *mut _) -> ()),
link_name,
abi,
args,
)?;
let handle = this.read_scalar(handle)?.to_i32()?;
let buf = this.read_pointer(buf)?;
let len = this.read_target_usize(len)?;
let ret_area = this.read_pointer(ret_area)?;
if len > 4096 {
throw_unsup_format!(
"wasm output-stream.blocking-write-and-flush: buffer too big"
);
}
let len = usize::try_from(len).unwrap();
let Some(fd) = this.machine.fds.get(handle) else {
throw_unsup_format!(
"wasm output-stream.blocking-write-and-flush: unsupported handle"
);
};
fd.write(
this.machine.communicate(),
buf,
len,
this,
callback!(
@capture<'tcx> {
len: usize,
ret_area: Pointer,
}
|this, result: Result<usize, IoError>| {
if !matches!(result, Ok(l) if l == len) {
throw_unsup_format!("wasm output-stream.blocking-write-and-flush: returning errors is not supported");
}
// 0 in the first byte of the ret_area indicates success.
let ret = this.ptr_to_mplace(ret_area, this.machine.layouts.u8);
this.write_null(&ret)?;
interp_ok(())
}),
)?;
}
_ => return interp_ok(EmulateItemResult::NotSupported),
}
interp_ok(EmulateItemResult::NeedsReturn)
}
}

1
src/tools/miri/src/shims/wasi/mod.rs
View file

@ -1 +0,0 @@
pub mod foreign_items;

1
src/tools/miri/tests/fail/panic/tls_macro_drop_panic.stderr
View file

@ -4,5 +4,6 @@ ow
fatal runtime error: thread local panicked on drop, aborting
error: abnormal termination: the program aborted execution
error: aborting due to 1 previous error

35
src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr
View file

@ -1,9 +1,9 @@
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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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
@ -91,19 +91,34 @@ 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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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 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/core/src/sync/atomic.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 | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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

35
src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr
View file

@ -1,9 +1,9 @@
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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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
@ -91,19 +91,34 @@ 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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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 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/core/src/sync/atomic.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 | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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

35
src/tools/miri/tests/genmc/pass/std/empty_main.stderr
View file

@ -1,28 +1,43 @@
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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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 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/core/src/sync/atomic.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 | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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

35
src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr
View file

@ -1,9 +1,9 @@
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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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
@ -95,19 +95,34 @@ 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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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 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/core/src/sync/atomic.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 | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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

35
src/tools/miri/tests/genmc/pass/std/thread_locals.stderr
View file

@ -1,9 +1,9 @@
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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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
@ -78,19 +78,34 @@ 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/core/src/sync/atomic.rs:LL:CC
--> RUSTLIB/std/src/rt.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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 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/core/src/sync/atomic.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 | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
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

36
src/tools/miri/tests/pass/shims/x86/rounding-error.rs
View file

@ -11,25 +11,27 @@ use std::arch::x86_64::*;
use std::collections::HashSet;
fn main() {
let a = unsafe { _mm_setr_ps(4.0, 4.0, 4.0, 4.0) };
let exact = 0.5;
// max error: 2^-12.
let rel_error_bound = 1.0 / (1 << 12) as f32;
let mut vals = HashSet::new();
for _ in 0..50 {
unsafe {
// Compute the inverse square root of 4.0, four times.
let a = _mm_setr_ps(4.0, 4.0, 4.0, 4.0);
let exact = 0.5;
let r = _mm_rsqrt_ps(a);
let r: [f32; 4] = std::mem::transmute(r);
// Check the results.
for r in r {
vals.insert(r.to_bits());
// Ensure the relative error is less than 2^-12.
let rel_error = (r - exact) / exact;
let log_error = rel_error.abs().log2();
assert!(
rel_error == 0.0 || log_error < -12.0,
"got an error of {rel_error} = 2^{log_error}"
);
}
// Compute the inverse square root of 4.0, four times.
let r = unsafe { _mm_rsqrt_ps(a) };
let r: [f32; 4] = unsafe { std::mem::transmute(r) };
// Check the results.
for r in r {
vals.insert(r.to_bits());
// Ensure the relative error is no more than 2^-12.
let rel_error = (r - exact) / exact;
assert!(
rel_error.abs() <= rel_error_bound,
"correct result: {exact}, got: {r}\n\
that's a relative error of {rel_error} (= 2^{log_error})",
log_error = rel_error.abs().log2()
);
}
}
// Ensure we saw a bunch of different results.