1use std::fmt::{self, Write};
2use std::num::NonZero;
3use std::sync::Mutex;
4
5use rustc_abi::{Align, Size};
6use rustc_data_structures::fx::{FxBuildHasher, FxHashSet};
7use rustc_errors::{Diag, DiagMessage, Level};
8use rustc_span::{DUMMY_SP, Span, SpanData, Symbol};
9
10use crate::borrow_tracker::stacked_borrows::diagnostics::TagHistory;
11use crate::borrow_tracker::tree_borrows::diagnostics as tree_diagnostics;
12use crate::*;
13
14pub enum TerminationInfo {
16 Exit {
17 code: i32,
18 leak_check: bool,
19 },
20 Abort(String),
21 Interrupted,
23 UnsupportedInIsolation(String),
24 StackedBorrowsUb {
25 msg: String,
26 help: Vec<String>,
27 history: Option<TagHistory>,
28 },
29 TreeBorrowsUb {
30 title: String,
31 details: Vec<String>,
32 history: tree_diagnostics::HistoryData,
33 },
34 Int2PtrWithStrictProvenance,
35 GlobalDeadlock,
37 LocalDeadlock,
39 MultipleSymbolDefinitions {
40 link_name: Symbol,
41 first: SpanData,
42 first_crate: Symbol,
43 second: SpanData,
44 second_crate: Symbol,
45 },
46 SymbolShimClashing {
47 link_name: Symbol,
48 span: SpanData,
49 },
50 DataRace {
51 involves_non_atomic: bool,
52 ptr: interpret::Pointer<AllocId>,
53 op1: RacingOp,
54 op2: RacingOp,
55 extra: Option<&'static str>,
56 retag_explain: bool,
57 },
58 UnsupportedForeignItem(String),
59}
60
61pub struct RacingOp {
62 pub action: String,
63 pub thread_info: String,
64 pub span: SpanData,
65}
66
67impl fmt::Display for TerminationInfo {
68 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
69 use TerminationInfo::*;
70 match self {
71 Exit { code, .. } => write!(f, "the evaluated program completed with exit code {code}"),
72 Abort(msg) => write!(f, "{msg}"),
73 Interrupted => write!(f, "interpretation was interrupted"),
74 UnsupportedInIsolation(msg) => write!(f, "{msg}"),
75 Int2PtrWithStrictProvenance =>
76 write!(
77 f,
78 "integer-to-pointer casts and `ptr::with_exposed_provenance` are not supported with `-Zmiri-strict-provenance`"
79 ),
80 StackedBorrowsUb { msg, .. } => write!(f, "{msg}"),
81 TreeBorrowsUb { title, .. } => write!(f, "{title}"),
82 GlobalDeadlock => write!(f, "the evaluated program deadlocked"),
83 LocalDeadlock => write!(f, "a thread deadlocked"),
84 MultipleSymbolDefinitions { link_name, .. } =>
85 write!(f, "multiple definitions of symbol `{link_name}`"),
86 SymbolShimClashing { link_name, .. } =>
87 write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
88 DataRace { involves_non_atomic, ptr, op1, op2, .. } =>
89 write!(
90 f,
91 "{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}",
92 if *involves_non_atomic { "Data race" } else { "Race condition" },
93 op1.action,
94 op1.thread_info,
95 op2.action,
96 op2.thread_info
97 ),
98 UnsupportedForeignItem(msg) => write!(f, "{msg}"),
99 }
100 }
101}
102
103impl fmt::Debug for TerminationInfo {
104 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
105 write!(f, "{self}")
106 }
107}
108
109impl MachineStopType for TerminationInfo {
110 fn diagnostic_message(&self) -> DiagMessage {
111 self.to_string().into()
112 }
113 fn add_args(
114 self: Box<Self>,
115 _: &mut dyn FnMut(std::borrow::Cow<'static, str>, rustc_errors::DiagArgValue),
116 ) {
117 }
118}
119
120pub enum NonHaltingDiagnostic {
122 CreatedPointerTag(NonZero<u64>, Option<String>, Option<(AllocId, AllocRange, ProvenanceExtra)>),
126 PoppedPointerTag(Item, String),
128 TrackingAlloc(AllocId, Size, Align),
129 FreedAlloc(AllocId),
130 AccessedAlloc(AllocId, AllocRange, borrow_tracker::AccessKind),
131 RejectedIsolatedOp(String),
132 ProgressReport {
133 block_count: u64, },
135 Int2Ptr {
136 details: bool,
137 },
138 NativeCallSharedMem {
139 tracing: bool,
140 },
141 WeakMemoryOutdatedLoad {
142 ptr: Pointer,
143 },
144 ExternTypeReborrow,
145 GenmcCompareExchangeWeak,
146 GenmcCompareExchangeOrderingMismatch {
147 success_ordering: AtomicRwOrd,
148 upgraded_success_ordering: AtomicRwOrd,
149 failure_ordering: AtomicReadOrd,
150 effective_failure_ordering: AtomicReadOrd,
151 },
152}
153
154pub enum DiagLevel {
156 Error,
157 Warning,
158 Note,
159}
160
161macro_rules! note {
163 ($($tt:tt)*) => { (None, format!($($tt)*)) };
164}
165macro_rules! note_span {
167 ($span:expr, $($tt:tt)*) => { (Some($span), format!($($tt)*)) };
168}
169
170pub fn prune_stacktrace<'tcx>(
174 mut stacktrace: Vec<FrameInfo<'tcx>>,
175 machine: &MiriMachine<'tcx>,
176) -> (Vec<FrameInfo<'tcx>>, bool) {
177 match machine.backtrace_style {
178 BacktraceStyle::Off => {
179 stacktrace.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
182 stacktrace.truncate(1);
184 (stacktrace, false)
185 }
186 BacktraceStyle::Short => {
187 let original_len = stacktrace.len();
188 stacktrace.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
191 let has_local_frame = stacktrace.iter().any(|frame| machine.is_local(frame.instance));
195 if has_local_frame {
196 stacktrace = stacktrace
201 .into_iter()
202 .take_while(|frame| {
203 let def_id = frame.instance.def_id();
204 let path = machine.tcx.def_path_str(def_id);
205 !path.contains("__rust_begin_short_backtrace")
206 })
207 .collect::<Vec<_>>();
208
209 while stacktrace.len() > 1
215 && stacktrace.last().is_some_and(|frame| !machine.is_local(frame.instance))
216 {
217 stacktrace.pop();
218 }
219 }
220 let was_pruned = stacktrace.len() != original_len;
221 (stacktrace, was_pruned)
222 }
223 BacktraceStyle::Full => (stacktrace, false),
224 }
225}
226
227pub fn report_result<'tcx>(
232 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
233 res: InterpErrorInfo<'tcx>,
234) -> Option<(i32, bool)> {
235 use InterpErrorKind::*;
236 use UndefinedBehaviorInfo::*;
237
238 let mut labels = vec![];
239
240 let (title, helps) = if let MachineStop(info) = res.kind() {
241 let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
242 use TerminationInfo::*;
243 let title = match info {
244 &Exit { code, leak_check } => return Some((code, leak_check)),
245 Abort(_) => Some("abnormal termination"),
246 Interrupted => None,
247 UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance | UnsupportedForeignItem(_) =>
248 Some("unsupported operation"),
249 StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
250 Some("Undefined Behavior"),
251 LocalDeadlock => {
252 labels.push(format!("thread got stuck here"));
253 None
254 }
255 GlobalDeadlock => {
256 let mut any_pruned = false;
259 for (thread, stack) in ecx.machine.threads.all_blocked_stacks() {
260 let stacktrace = Frame::generate_stacktrace_from_stack(stack);
261 let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
262 any_pruned |= was_pruned;
263 report_msg(
264 DiagLevel::Error,
265 format!("the evaluated program deadlocked"),
266 vec![format!("thread got stuck here")],
267 vec![],
268 vec![],
269 &stacktrace,
270 Some(thread),
271 &ecx.machine,
272 )
273 }
274 if any_pruned {
275 ecx.tcx.dcx().note(
276 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace"
277 );
278 }
279 return None;
280 }
281 MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
282 };
283 #[rustfmt::skip]
284 let helps = match info {
285 UnsupportedInIsolation(_) =>
286 vec![
287 note!("set `MIRIFLAGS=-Zmiri-disable-isolation` to disable isolation;"),
288 note!("or set `MIRIFLAGS=-Zmiri-isolation-error=warn` to make Miri return an error code from isolated operations (if supported for that operation) and continue with a warning"),
289 ],
290 UnsupportedForeignItem(_) => {
291 vec![
292 note!("this means the program tried to do something Miri does not support; it does not indicate a bug in the program"),
293 ]
294 }
295 StackedBorrowsUb { help, history, .. } => {
296 labels.extend(help.clone());
297 let mut helps = vec![
298 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental"),
299 note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information"),
300 ];
301 if let Some(TagHistory {created, invalidated, protected}) = history.clone() {
302 helps.push((Some(created.1), created.0));
303 if let Some((msg, span)) = invalidated {
304 helps.push(note_span!(span, "{msg}"));
305 }
306 if let Some((protector_msg, protector_span)) = protected {
307 helps.push(note_span!(protector_span, "{protector_msg}"));
308 }
309 }
310 helps
311 },
312 TreeBorrowsUb { title: _, details, history } => {
313 let mut helps = vec![
314 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental"),
315 note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information"),
316 ];
317 for m in details {
318 helps.push(note!("{m}"));
319 }
320 for event in history.events.clone() {
321 helps.push(event);
322 }
323 helps
324 }
325 MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
326 vec![
327 note_span!(*first, "it's first defined here, in crate `{first_crate}`"),
328 note_span!(*second, "then it's defined here again, in crate `{second_crate}`"),
329 ],
330 SymbolShimClashing { link_name, span } =>
331 vec![note_span!(*span, "the `{link_name}` symbol is defined here")],
332 Int2PtrWithStrictProvenance =>
333 vec![note!("use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead")],
334 DataRace { op1, extra, retag_explain, .. } => {
335 labels.push(format!("(2) just happened here"));
336 let mut helps = vec![note_span!(op1.span, "and (1) occurred earlier here")];
337 if let Some(extra) = extra {
338 helps.push(note!("{extra}"));
339 helps.push(note!("see https://doc.rust-lang.org/nightly/std/sync/atomic/index.html#memory-model-for-atomic-accesses for more information about the Rust memory model"));
340 }
341 if *retag_explain {
342 helps.push(note!("retags occur on all (re)borrows and as well as when references are copied or moved"));
343 helps.push(note!("retags permit optimizations that insert speculative reads or writes"));
344 helps.push(note!("therefore from the perspective of data races, a retag has the same implications as a read or write"));
345 }
346 helps.push(note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"));
347 helps.push(note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"));
348 helps
349 }
350 ,
351 _ => vec![],
352 };
353 (title, helps)
354 } else {
355 let title = match res.kind() {
356 UndefinedBehavior(ValidationError(validation_err))
357 if matches!(
358 validation_err.kind,
359 ValidationErrorKind::PointerAsInt { .. } | ValidationErrorKind::PartialPointer
360 ) =>
361 {
362 ecx.handle_ice(); bug!(
364 "This validation error should be impossible in Miri: {}",
365 format_interp_error(ecx.tcx.dcx(), res)
366 );
367 }
368 UndefinedBehavior(_) => "Undefined Behavior",
369 ResourceExhaustion(_) => "resource exhaustion",
370 Unsupported(
371 UnsupportedOpInfo::Unsupported(_)
373 | UnsupportedOpInfo::UnsizedLocal
374 | UnsupportedOpInfo::ExternTypeField,
375 ) => "unsupported operation",
376 InvalidProgram(
377 InvalidProgramInfo::AlreadyReported(_) | InvalidProgramInfo::Layout(..),
379 ) => "post-monomorphization error",
380 _ => {
381 ecx.handle_ice(); bug!(
383 "This error should be impossible in Miri: {}",
384 format_interp_error(ecx.tcx.dcx(), res)
385 );
386 }
387 };
388 #[rustfmt::skip]
389 let helps = match res.kind() {
390 Unsupported(_) =>
391 vec![
392 note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
393 ],
394 ResourceExhaustion(ResourceExhaustionInfo::AddressSpaceFull) if ecx.machine.data_race.as_genmc_ref().is_some() =>
395 vec![
396 note!("in GenMC mode, the address space is limited to 4GB per thread, and addresses cannot be reused")
397 ],
398 UndefinedBehavior(AlignmentCheckFailed { .. })
399 if ecx.machine.check_alignment == AlignmentCheck::Symbolic
400 =>
401 vec![
402 note!("this usually indicates that your program performed an invalid operation and caused Undefined Behavior"),
403 note!("but due to `-Zmiri-symbolic-alignment-check`, alignment errors can also be false positives"),
404 ],
405 UndefinedBehavior(info) => {
406 let mut helps = vec![
407 note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"),
408 note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"),
409 ];
410 match info {
411 PointerUseAfterFree(alloc_id, _) | PointerOutOfBounds { alloc_id, .. } => {
412 if let Some(span) = ecx.machine.allocated_span(*alloc_id) {
413 helps.push(note_span!(span, "{:?} was allocated here:", alloc_id));
414 }
415 if let Some(span) = ecx.machine.deallocated_span(*alloc_id) {
416 helps.push(note_span!(span, "{:?} was deallocated here:", alloc_id));
417 }
418 }
419 AbiMismatchArgument { .. } | AbiMismatchReturn { .. } => {
420 helps.push(note!("this means these two types are not *guaranteed* to be ABI-compatible across all targets"));
421 helps.push(note!("if you think this code should be accepted anyway, please report an issue with Miri"));
422 }
423 _ => {},
424 }
425 helps
426 }
427 InvalidProgram(
428 InvalidProgramInfo::AlreadyReported(_)
429 ) => {
430 return None;
432 }
433 _ =>
434 vec![],
435 };
436 (Some(title), helps)
437 };
438
439 let stacktrace = ecx.generate_stacktrace();
440 let (stacktrace, pruned) = prune_stacktrace(stacktrace, &ecx.machine);
441
442 let mut extra = String::new();
445 match res.kind() {
446 UndefinedBehavior(InvalidUninitBytes(Some((alloc_id, access)))) => {
447 writeln!(
448 extra,
449 "Uninitialized memory occurred at {alloc_id:?}{range:?}, in this allocation:",
450 range = access.bad,
451 )
452 .unwrap();
453 writeln!(extra, "{:?}", ecx.dump_alloc(*alloc_id)).unwrap();
454 }
455 _ => {}
456 }
457
458 let mut primary_msg = String::new();
459 if let Some(title) = title {
460 write!(primary_msg, "{title}: ").unwrap();
461 }
462 write!(primary_msg, "{}", format_interp_error(ecx.tcx.dcx(), res)).unwrap();
463
464 if labels.is_empty() {
465 labels.push(format!(
466 "{} occurred {}",
467 title.unwrap_or("error"),
468 if stacktrace.is_empty() { "due to this code" } else { "here" }
469 ));
470 }
471
472 report_msg(
473 DiagLevel::Error,
474 primary_msg,
475 labels,
476 vec![],
477 helps,
478 &stacktrace,
479 Some(ecx.active_thread()),
480 &ecx.machine,
481 );
482
483 eprint!("{extra}"); if pruned {
487 ecx.tcx.dcx().note(
488 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
489 );
490 }
491
492 for (i, frame) in ecx.active_thread_stack().iter().enumerate() {
494 trace!("-------------------");
495 trace!("Frame {}", i);
496 trace!(" return: {:?}", frame.return_place);
497 for (i, local) in frame.locals.iter().enumerate() {
498 trace!(" local {}: {:?}", i, local);
499 }
500 }
501
502 None
503}
504
505pub fn report_leaks<'tcx>(
506 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
507 leaks: Vec<(AllocId, MemoryKind, Allocation<Provenance, AllocExtra<'tcx>, MiriAllocBytes>)>,
508) {
509 let mut any_pruned = false;
510 for (id, kind, alloc) in leaks {
511 let mut title = format!(
512 "memory leaked: {id:?} ({}, size: {:?}, align: {:?})",
513 kind,
514 alloc.size().bytes(),
515 alloc.align.bytes()
516 );
517 let Some(backtrace) = alloc.extra.backtrace else {
518 ecx.tcx.dcx().err(title);
519 continue;
520 };
521 title.push_str(", allocated here:");
522 let (backtrace, pruned) = prune_stacktrace(backtrace, &ecx.machine);
523 any_pruned |= pruned;
524 report_msg(
525 DiagLevel::Error,
526 title,
527 vec![],
528 vec![],
529 vec![],
530 &backtrace,
531 None, &ecx.machine,
533 );
534 }
535 if any_pruned {
536 ecx.tcx.dcx().note(
537 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
538 );
539 }
540}
541
542fn report_msg<'tcx>(
548 diag_level: DiagLevel,
549 title: String,
550 span_msg: Vec<String>,
551 notes: Vec<(Option<SpanData>, String)>,
552 helps: Vec<(Option<SpanData>, String)>,
553 stacktrace: &[FrameInfo<'tcx>],
554 thread: Option<ThreadId>,
555 machine: &MiriMachine<'tcx>,
556) {
557 let origin_span = thread.map(|t| machine.threads.thread_ref(t).origin_span).unwrap_or(DUMMY_SP);
558 let span = stacktrace.first().map(|fi| fi.span).unwrap_or(origin_span);
559 assert!(!span.is_dummy());
562
563 let tcx = machine.tcx;
564 let level = match diag_level {
565 DiagLevel::Error => Level::Error,
566 DiagLevel::Warning => Level::Warning,
567 DiagLevel::Note => Level::Note,
568 };
569 let mut err = Diag::<()>::new(tcx.sess.dcx(), level, title);
570 err.span(span);
571
572 for line in span_msg {
574 err.span_label(span, line);
575 }
576
577 for (span_data, note) in notes {
579 if let Some(span_data) = span_data {
580 err.span_note(span_data.span(), note);
581 } else {
582 err.note(note);
583 }
584 }
585 for (span_data, help) in helps {
586 if let Some(span_data) = span_data {
587 err.span_help(span_data.span(), help);
588 } else {
589 err.help(help);
590 }
591 }
592 if let Some(thread) = thread
594 && machine.threads.get_total_thread_count() > 1
595 {
596 err.note(format!(
597 "this is on thread `{}`",
598 machine.threads.get_thread_display_name(thread)
599 ));
600 }
601
602 if stacktrace.len() > 0 {
604 if stacktrace.len() > 1 {
606 let sm = tcx.sess.source_map();
607 let mut out = format!("stack backtrace:");
608 for (idx, frame_info) in stacktrace.iter().enumerate() {
609 let span = sm.span_to_diagnostic_string(frame_info.span);
610 write!(out, "\n{idx}: {}", frame_info.instance).unwrap();
611 write!(out, "\n at {span}").unwrap();
612 }
613 err.note(out);
614 }
615 if !origin_span.is_dummy() {
617 let what = if stacktrace.len() > 1 {
618 "the last function in that backtrace"
619 } else {
620 "the current function"
621 };
622 err.span_note(origin_span, format!("{what} got called indirectly due to this code"));
623 }
624 } else if !span.is_dummy() {
625 err.note(format!("this {level} occurred while pushing a call frame onto an empty stack"));
626 err.note("the span indicates which code caused the function to be called, but may not be the literal call site");
627 }
628
629 err.emit();
630}
631
632impl<'tcx> MiriMachine<'tcx> {
633 pub fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
634 use NonHaltingDiagnostic::*;
635
636 let stacktrace = Frame::generate_stacktrace_from_stack(self.threads.active_thread_stack());
637 let (stacktrace, _was_pruned) = prune_stacktrace(stacktrace, self);
638
639 let (label, diag_level) = match &e {
640 RejectedIsolatedOp(_) =>
641 ("operation rejected by isolation".to_string(), DiagLevel::Warning),
642 Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning),
643 NativeCallSharedMem { .. } =>
644 ("sharing memory with a native function".to_string(), DiagLevel::Warning),
645 ExternTypeReborrow =>
646 ("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
647 GenmcCompareExchangeWeak | GenmcCompareExchangeOrderingMismatch { .. } =>
648 ("GenMC might miss possible behaviors of this code".to_string(), DiagLevel::Warning),
649 CreatedPointerTag(..)
650 | PoppedPointerTag(..)
651 | TrackingAlloc(..)
652 | AccessedAlloc(..)
653 | FreedAlloc(..)
654 | ProgressReport { .. }
655 | WeakMemoryOutdatedLoad { .. } =>
656 ("tracking was triggered here".to_string(), DiagLevel::Note),
657 };
658
659 let title = match &e {
660 CreatedPointerTag(tag, None, _) => format!("created base tag {tag:?}"),
661 CreatedPointerTag(tag, Some(perm), None) =>
662 format!("created {tag:?} with {perm} derived from unknown tag"),
663 CreatedPointerTag(tag, Some(perm), Some((alloc_id, range, orig_tag))) =>
664 format!(
665 "created tag {tag:?} with {perm} at {alloc_id:?}{range:?} derived from {orig_tag:?}"
666 ),
667 PoppedPointerTag(item, cause) => format!("popped tracked tag for item {item:?}{cause}"),
668 TrackingAlloc(id, size, align) =>
669 format!(
670 "now tracking allocation {id:?} of {size} bytes (alignment {align} bytes)",
671 size = size.bytes(),
672 align = align.bytes(),
673 ),
674 AccessedAlloc(id, range, access_kind) =>
675 format!("{access_kind} at {id:?}[{}..{}]", range.start.bytes(), range.end().bytes()),
676 FreedAlloc(id) => format!("freed allocation {id:?}"),
677 RejectedIsolatedOp(op) => format!("{op} was made to return an error due to isolation"),
678 ProgressReport { .. } =>
679 format!("progress report: current operation being executed is here"),
680 Int2Ptr { .. } => format!("integer-to-pointer cast"),
681 NativeCallSharedMem { .. } =>
682 format!("sharing memory with a native function called via FFI"),
683 WeakMemoryOutdatedLoad { ptr } =>
684 format!("weak memory emulation: outdated value returned from load at {ptr}"),
685 ExternTypeReborrow =>
686 format!("reborrow of a reference to `extern type` is not properly supported"),
687 GenmcCompareExchangeWeak =>
688 "GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures."
689 .to_string(),
690 GenmcCompareExchangeOrderingMismatch {
691 success_ordering,
692 upgraded_success_ordering,
693 failure_ordering,
694 effective_failure_ordering,
695 } => {
696 let was_upgraded_msg = if success_ordering != upgraded_success_ordering {
697 format!("Success ordering '{success_ordering:?}' was upgraded to '{upgraded_success_ordering:?}' to match failure ordering '{failure_ordering:?}'")
698 } else {
699 assert_ne!(failure_ordering, effective_failure_ordering);
700 format!("Due to success ordering '{success_ordering:?}', the failure ordering '{failure_ordering:?}' is treated like '{effective_failure_ordering:?}'")
701 };
702 format!("GenMC currently does not model the failure ordering for `compare_exchange`. {was_upgraded_msg}. Miri with GenMC might miss bugs related to this memory access.")
703 }
704 };
705
706 let notes = match &e {
707 ProgressReport { block_count } => {
708 vec![note!("so far, {block_count} basic blocks have been executed")]
709 }
710 _ => vec![],
711 };
712
713 let helps = match &e {
714 Int2Ptr { details: true } => {
715 let mut v = vec![
716 note!(
717 "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"
718 ),
719 note!(
720 "see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation"
721 ),
722 note!(
723 "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"
724 ),
725 note!(
726 "you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics"
727 ),
728 ];
729 if self.borrow_tracker.as_ref().is_some_and(|b| {
730 matches!(
731 b.borrow().borrow_tracker_method(),
732 BorrowTrackerMethod::TreeBorrows { .. }
733 )
734 }) {
735 v.push(
736 note!("Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used")
737 );
738 } else {
739 v.push(
740 note!("alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning")
741 );
742 }
743 v
744 }
745 NativeCallSharedMem { tracing } =>
746 if *tracing {
747 vec![
748 note!(
749 "when memory is shared with a native function call, Miri can only track initialisation and provenance on a best-effort basis"
750 ),
751 note!(
752 "in particular, Miri assumes that the native call initializes all memory it has written to"
753 ),
754 note!(
755 "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory"
756 ),
757 note!(
758 "what this means is that Miri will easily miss Undefined Behavior related to incorrect usage of this shared memory, so you should not take a clean Miri run as a signal that your FFI code is UB-free"
759 ),
760 note!(
761 "tracing memory accesses in native code is not yet fully implemented, so there can be further imprecisions beyond what is documented here"
762 ),
763 ]
764 } else {
765 vec![
766 note!(
767 "when memory is shared with a native function call, Miri stops tracking initialization and provenance for that memory"
768 ),
769 note!(
770 "in particular, Miri assumes that the native call initializes all memory it has access to"
771 ),
772 note!(
773 "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory"
774 ),
775 note!(
776 "what this means is that Miri will easily miss Undefined Behavior related to incorrect usage of this shared memory, so you should not take a clean Miri run as a signal that your FFI code is UB-free"
777 ),
778 ]
779 },
780 ExternTypeReborrow => {
781 assert!(self.borrow_tracker.as_ref().is_some_and(|b| {
782 matches!(
783 b.borrow().borrow_tracker_method(),
784 BorrowTrackerMethod::StackedBorrows
785 )
786 }));
787 vec![
788 note!(
789 "`extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code"
790 ),
791 note!(
792 "try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead"
793 ),
794 ]
795 }
796 _ => vec![],
797 };
798
799 report_msg(
800 diag_level,
801 title,
802 vec![label],
803 notes,
804 helps,
805 &stacktrace,
806 Some(self.threads.active_thread()),
807 self,
808 );
809 }
810}
811
812impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
813pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
814 fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
815 let this = self.eval_context_ref();
816 this.machine.emit_diagnostic(e);
817 }
818
819 fn handle_ice(&self) {
821 eprintln!();
822 eprintln!(
823 "Miri caused an ICE during evaluation. Here's the interpreter backtrace at the time of the panic:"
824 );
825 let this = self.eval_context_ref();
826 let stacktrace = this.generate_stacktrace();
827 report_msg(
828 DiagLevel::Note,
829 "the place in the program where the ICE was triggered".to_string(),
830 vec![],
831 vec![],
832 vec![],
833 &stacktrace,
834 Some(this.active_thread()),
835 &this.machine,
836 );
837 }
838
839 fn dedup_diagnostic(
843 &self,
844 dedup: &SpanDedupDiagnostic,
845 f: impl FnOnce(bool) -> NonHaltingDiagnostic,
846 ) {
847 let this = self.eval_context_ref();
848 let span1 = this.machine.current_user_relevant_span();
852 let span2 = this
855 .active_thread_stack()
856 .iter()
857 .rev()
858 .find(|frame| !frame.instance().def.requires_caller_location(*this.tcx))
859 .map(|frame| frame.current_span())
860 .unwrap_or(span1);
861
862 let mut lock = dedup.0.lock().unwrap();
863 let first = lock.is_empty();
864 if !lock.contains(&span2) && lock.insert(span1) && (span1 == span2 || lock.insert(span2)) {
866 this.emit_diagnostic(f(first));
868 }
869 }
870}
871
872pub struct SpanDedupDiagnostic(Mutex<FxHashSet<Span>>);
874
875impl SpanDedupDiagnostic {
876 pub const fn new() -> Self {
877 Self(Mutex::new(FxHashSet::with_hasher(FxBuildHasher)))
878 }
879}