1use std::fmt::{self, Write};
2use std::num::NonZero;
3
4use rustc_abi::{Align, Size};
5use rustc_errors::{Diag, DiagMessage, Level};
6use rustc_span::{DUMMY_SP, SpanData, Symbol};
7
8use crate::borrow_tracker::stacked_borrows::diagnostics::TagHistory;
9use crate::borrow_tracker::tree_borrows::diagnostics as tree_diagnostics;
10use crate::*;
11
12pub enum TerminationInfo {
14 Exit {
15 code: i32,
16 leak_check: bool,
17 },
18 Abort(String),
19 Interrupted,
21 UnsupportedInIsolation(String),
22 StackedBorrowsUb {
23 msg: String,
24 help: Vec<String>,
25 history: Option<TagHistory>,
26 },
27 TreeBorrowsUb {
28 title: String,
29 details: Vec<String>,
30 history: tree_diagnostics::HistoryData,
31 },
32 Int2PtrWithStrictProvenance,
33 Deadlock,
34 GenmcBlockedExecution,
37 MultipleSymbolDefinitions {
38 link_name: Symbol,
39 first: SpanData,
40 first_crate: Symbol,
41 second: SpanData,
42 second_crate: Symbol,
43 },
44 SymbolShimClashing {
45 link_name: Symbol,
46 span: SpanData,
47 },
48 DataRace {
49 involves_non_atomic: bool,
50 ptr: interpret::Pointer<AllocId>,
51 op1: RacingOp,
52 op2: RacingOp,
53 extra: Option<&'static str>,
54 retag_explain: bool,
55 },
56 UnsupportedForeignItem(String),
57}
58
59pub struct RacingOp {
60 pub action: String,
61 pub thread_info: String,
62 pub span: SpanData,
63}
64
65impl fmt::Display for TerminationInfo {
66 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
67 use TerminationInfo::*;
68 match self {
69 Exit { code, .. } => write!(f, "the evaluated program completed with exit code {code}"),
70 Abort(msg) => write!(f, "{msg}"),
71 Interrupted => write!(f, "interpretation was interrupted"),
72 UnsupportedInIsolation(msg) => write!(f, "{msg}"),
73 Int2PtrWithStrictProvenance =>
74 write!(
75 f,
76 "integer-to-pointer casts and `ptr::with_exposed_provenance` are not supported with `-Zmiri-strict-provenance`"
77 ),
78 StackedBorrowsUb { msg, .. } => write!(f, "{msg}"),
79 TreeBorrowsUb { title, .. } => write!(f, "{title}"),
80 Deadlock => write!(f, "the evaluated program deadlocked"),
81 GenmcBlockedExecution =>
82 write!(f, "GenMC determined that the execution got blocked (this is not an error)"),
83 MultipleSymbolDefinitions { link_name, .. } =>
84 write!(f, "multiple definitions of symbol `{link_name}`"),
85 SymbolShimClashing { link_name, .. } =>
86 write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
87 DataRace { involves_non_atomic, ptr, op1, op2, .. } =>
88 write!(
89 f,
90 "{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}",
91 if *involves_non_atomic { "Data race" } else { "Race condition" },
92 op1.action,
93 op1.thread_info,
94 op2.action,
95 op2.thread_info
96 ),
97 UnsupportedForeignItem(msg) => write!(f, "{msg}"),
98 }
99 }
100}
101
102impl fmt::Debug for TerminationInfo {
103 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
104 write!(f, "{self}")
105 }
106}
107
108impl MachineStopType for TerminationInfo {
109 fn diagnostic_message(&self) -> DiagMessage {
110 self.to_string().into()
111 }
112 fn add_args(
113 self: Box<Self>,
114 _: &mut dyn FnMut(std::borrow::Cow<'static, str>, rustc_errors::DiagArgValue),
115 ) {
116 }
117}
118
119pub enum NonHaltingDiagnostic {
121 CreatedPointerTag(NonZero<u64>, Option<String>, Option<(AllocId, AllocRange, ProvenanceExtra)>),
125 PoppedPointerTag(Item, String),
127 CreatedAlloc(AllocId, Size, Align, MemoryKind),
128 FreedAlloc(AllocId),
129 AccessedAlloc(AllocId, AccessKind),
130 RejectedIsolatedOp(String),
131 ProgressReport {
132 block_count: u64, },
134 Int2Ptr {
135 details: bool,
136 },
137 NativeCallSharedMem {
138 tracing: bool,
139 },
140 WeakMemoryOutdatedLoad {
141 ptr: Pointer,
142 },
143 ExternTypeReborrow,
144 GenmcCompareExchangeWeak,
145 GenmcCompareExchangeOrderingMismatch {
146 success_ordering: AtomicRwOrd,
147 upgraded_success_ordering: AtomicRwOrd,
148 failure_ordering: AtomicReadOrd,
149 effective_failure_ordering: AtomicReadOrd,
150 },
151}
152
153pub enum DiagLevel {
155 Error,
156 Warning,
157 Note,
158}
159
160macro_rules! note {
162 ($($tt:tt)*) => { (None, format!($($tt)*)) };
163}
164macro_rules! note_span {
166 ($span:expr, $($tt:tt)*) => { (Some($span), format!($($tt)*)) };
167}
168
169pub fn prune_stacktrace<'tcx>(
173 mut stacktrace: Vec<FrameInfo<'tcx>>,
174 machine: &MiriMachine<'tcx>,
175) -> (Vec<FrameInfo<'tcx>>, bool) {
176 match machine.backtrace_style {
177 BacktraceStyle::Off => {
178 stacktrace.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
181 stacktrace.truncate(1);
183 (stacktrace, false)
184 }
185 BacktraceStyle::Short => {
186 let original_len = stacktrace.len();
187 let has_local_frame = stacktrace.iter().any(|frame| machine.is_local(frame));
191 if has_local_frame {
192 stacktrace
195 .retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
196
197 stacktrace = stacktrace
202 .into_iter()
203 .take_while(|frame| {
204 let def_id = frame.instance.def_id();
205 let path = machine.tcx.def_path_str(def_id);
206 !path.contains("__rust_begin_short_backtrace")
207 })
208 .collect::<Vec<_>>();
209
210 while stacktrace.len() > 1
216 && stacktrace.last().is_some_and(|frame| !machine.is_local(frame))
217 {
218 stacktrace.pop();
219 }
220 }
221 let was_pruned = stacktrace.len() != original_len;
222 (stacktrace, was_pruned)
223 }
224 BacktraceStyle::Full => (stacktrace, false),
225 }
226}
227
228pub fn report_error<'tcx>(
232 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
233 e: 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) = e.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 Deadlock => {
252 labels.push(format!("this thread got stuck here"));
253 None
254 }
255 GenmcBlockedExecution => {
256 assert!(ecx.machine.data_race.as_genmc_ref().is_some());
258 return Some((0, false));
261 }
262 MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
263 };
264 #[rustfmt::skip]
265 let helps = match info {
266 UnsupportedInIsolation(_) =>
267 vec![
268 note!("set `MIRIFLAGS=-Zmiri-disable-isolation` to disable isolation;"),
269 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"),
270 ],
271 UnsupportedForeignItem(_) => {
272 vec![
273 note!("this means the program tried to do something Miri does not support; it does not indicate a bug in the program"),
274 ]
275 }
276 StackedBorrowsUb { help, history, .. } => {
277 labels.extend(help.clone());
278 let mut helps = vec![
279 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental"),
280 note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information"),
281 ];
282 if let Some(TagHistory {created, invalidated, protected}) = history.clone() {
283 helps.push((Some(created.1), created.0));
284 if let Some((msg, span)) = invalidated {
285 helps.push(note_span!(span, "{msg}"));
286 }
287 if let Some((protector_msg, protector_span)) = protected {
288 helps.push(note_span!(protector_span, "{protector_msg}"));
289 }
290 }
291 helps
292 },
293 TreeBorrowsUb { title: _, details, history } => {
294 let mut helps = vec![
295 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental"),
296 note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information"),
297 ];
298 for m in details {
299 helps.push(note!("{m}"));
300 }
301 for event in history.events.clone() {
302 helps.push(event);
303 }
304 helps
305 }
306 MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
307 vec![
308 note_span!(*first, "it's first defined here, in crate `{first_crate}`"),
309 note_span!(*second, "then it's defined here again, in crate `{second_crate}`"),
310 ],
311 SymbolShimClashing { link_name, span } =>
312 vec![note_span!(*span, "the `{link_name}` symbol is defined here")],
313 Int2PtrWithStrictProvenance =>
314 vec![note!("use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead")],
315 DataRace { op1, extra, retag_explain, .. } => {
316 labels.push(format!("(2) just happened here"));
317 let mut helps = vec![note_span!(op1.span, "and (1) occurred earlier here")];
318 if let Some(extra) = extra {
319 helps.push(note!("{extra}"));
320 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"));
321 }
322 if *retag_explain {
323 helps.push(note!("retags occur on all (re)borrows and as well as when references are copied or moved"));
324 helps.push(note!("retags permit optimizations that insert speculative reads or writes"));
325 helps.push(note!("therefore from the perspective of data races, a retag has the same implications as a read or write"));
326 }
327 helps.push(note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"));
328 helps.push(note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"));
329 helps
330 }
331 ,
332 _ => vec![],
333 };
334 (title, helps)
335 } else {
336 let title = match e.kind() {
337 UndefinedBehavior(ValidationError(validation_err))
338 if matches!(
339 validation_err.kind,
340 ValidationErrorKind::PointerAsInt { .. } | ValidationErrorKind::PartialPointer
341 ) =>
342 {
343 ecx.handle_ice(); bug!(
345 "This validation error should be impossible in Miri: {}",
346 format_interp_error(ecx.tcx.dcx(), e)
347 );
348 }
349 UndefinedBehavior(_) => "Undefined Behavior",
350 ResourceExhaustion(_) => "resource exhaustion",
351 Unsupported(
352 UnsupportedOpInfo::Unsupported(_)
354 | UnsupportedOpInfo::UnsizedLocal
355 | UnsupportedOpInfo::ExternTypeField,
356 ) => "unsupported operation",
357 InvalidProgram(
358 InvalidProgramInfo::AlreadyReported(_) | InvalidProgramInfo::Layout(..),
360 ) => "post-monomorphization error",
361 _ => {
362 ecx.handle_ice(); bug!(
364 "This error should be impossible in Miri: {}",
365 format_interp_error(ecx.tcx.dcx(), e)
366 );
367 }
368 };
369 #[rustfmt::skip]
370 let helps = match e.kind() {
371 Unsupported(_) =>
372 vec![
373 note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
374 ],
375 UndefinedBehavior(AlignmentCheckFailed { .. })
376 if ecx.machine.check_alignment == AlignmentCheck::Symbolic
377 =>
378 vec![
379 note!("this usually indicates that your program performed an invalid operation and caused Undefined Behavior"),
380 note!("but due to `-Zmiri-symbolic-alignment-check`, alignment errors can also be false positives"),
381 ],
382 UndefinedBehavior(info) => {
383 let mut helps = vec![
384 note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"),
385 note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"),
386 ];
387 match info {
388 PointerUseAfterFree(alloc_id, _) | PointerOutOfBounds { alloc_id, .. } => {
389 if let Some(span) = ecx.machine.allocated_span(*alloc_id) {
390 helps.push(note_span!(span, "{:?} was allocated here:", alloc_id));
391 }
392 if let Some(span) = ecx.machine.deallocated_span(*alloc_id) {
393 helps.push(note_span!(span, "{:?} was deallocated here:", alloc_id));
394 }
395 }
396 AbiMismatchArgument { .. } | AbiMismatchReturn { .. } => {
397 helps.push(note!("this means these two types are not *guaranteed* to be ABI-compatible across all targets"));
398 helps.push(note!("if you think this code should be accepted anyway, please report an issue with Miri"));
399 }
400 _ => {},
401 }
402 helps
403 }
404 InvalidProgram(
405 InvalidProgramInfo::AlreadyReported(_)
406 ) => {
407 return None;
409 }
410 _ =>
411 vec![],
412 };
413 (Some(title), helps)
414 };
415
416 let stacktrace = ecx.generate_stacktrace();
417 let (stacktrace, mut any_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
418
419 let mut show_all_threads = false;
420
421 let mut extra = String::new();
424 match e.kind() {
425 UndefinedBehavior(InvalidUninitBytes(Some((alloc_id, access)))) => {
426 writeln!(
427 extra,
428 "Uninitialized memory occurred at {alloc_id:?}{range:?}, in this allocation:",
429 range = access.bad,
430 )
431 .unwrap();
432 writeln!(extra, "{:?}", ecx.dump_alloc(*alloc_id)).unwrap();
433 }
434 MachineStop(info) => {
435 let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
436 match info {
437 TerminationInfo::Deadlock => {
438 show_all_threads = true;
439 }
440 _ => {}
441 }
442 }
443 _ => {}
444 }
445
446 let mut primary_msg = String::new();
447 if let Some(title) = title {
448 write!(primary_msg, "{title}: ").unwrap();
449 }
450 write!(primary_msg, "{}", format_interp_error(ecx.tcx.dcx(), e)).unwrap();
451
452 if labels.is_empty() {
453 labels.push(format!("{} occurred here", title.unwrap_or("error")));
454 }
455
456 report_msg(
457 DiagLevel::Error,
458 primary_msg,
459 labels,
460 vec![],
461 helps,
462 &stacktrace,
463 Some(ecx.active_thread()),
464 &ecx.machine,
465 );
466
467 eprint!("{extra}"); if show_all_threads {
470 for (thread, stack) in ecx.machine.threads.all_stacks() {
471 if thread != ecx.active_thread() {
472 let stacktrace = Frame::generate_stacktrace_from_stack(stack);
473 let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
474 any_pruned |= was_pruned;
475 report_msg(
476 DiagLevel::Error,
477 format!("the evaluated program deadlocked"),
478 vec![format!("this thread got stuck here")],
479 vec![],
480 vec![],
481 &stacktrace,
482 Some(thread),
483 &ecx.machine,
484 )
485 }
486 }
487 }
488
489 if any_pruned {
491 ecx.tcx.dcx().note(
492 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
493 );
494 }
495
496 for (i, frame) in ecx.active_thread_stack().iter().enumerate() {
498 trace!("-------------------");
499 trace!("Frame {}", i);
500 trace!(" return: {:?}", frame.return_place);
501 for (i, local) in frame.locals.iter().enumerate() {
502 trace!(" local {}: {:?}", i, local);
503 }
504 }
505
506 None
507}
508
509pub fn report_leaks<'tcx>(
510 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
511 leaks: Vec<(AllocId, MemoryKind, Allocation<Provenance, AllocExtra<'tcx>, MiriAllocBytes>)>,
512) {
513 let mut any_pruned = false;
514 for (id, kind, alloc) in leaks {
515 let mut title = format!(
516 "memory leaked: {id:?} ({}, size: {:?}, align: {:?})",
517 kind,
518 alloc.size().bytes(),
519 alloc.align.bytes()
520 );
521 let Some(backtrace) = alloc.extra.backtrace else {
522 ecx.tcx.dcx().err(title);
523 continue;
524 };
525 title.push_str(", allocated here:");
526 let (backtrace, pruned) = prune_stacktrace(backtrace, &ecx.machine);
527 any_pruned |= pruned;
528 report_msg(
529 DiagLevel::Error,
530 title,
531 vec![],
532 vec![],
533 vec![],
534 &backtrace,
535 None, &ecx.machine,
537 );
538 }
539 if any_pruned {
540 ecx.tcx.dcx().note(
541 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
542 );
543 }
544}
545
546pub fn report_msg<'tcx>(
552 diag_level: DiagLevel,
553 title: String,
554 span_msg: Vec<String>,
555 notes: Vec<(Option<SpanData>, String)>,
556 helps: Vec<(Option<SpanData>, String)>,
557 stacktrace: &[FrameInfo<'tcx>],
558 thread: Option<ThreadId>,
559 machine: &MiriMachine<'tcx>,
560) {
561 let span = stacktrace.first().map_or(DUMMY_SP, |fi| fi.span);
562 let sess = machine.tcx.sess;
563 let level = match diag_level {
564 DiagLevel::Error => Level::Error,
565 DiagLevel::Warning => Level::Warning,
566 DiagLevel::Note => Level::Note,
567 };
568 let mut err = Diag::<()>::new(sess.dcx(), level, title);
569 err.span(span);
570
571 if span != DUMMY_SP {
573 for line in span_msg {
574 err.span_label(span, line);
575 }
576 } else {
577 for line in span_msg {
579 err.note(line);
580 }
581 err.note("(no span available)");
582 }
583
584 let mut extra_span = false;
586 for (span_data, note) in notes {
587 if let Some(span_data) = span_data {
588 err.span_note(span_data.span(), note);
589 extra_span = true;
590 } else {
591 err.note(note);
592 }
593 }
594 for (span_data, help) in helps {
595 if let Some(span_data) = span_data {
596 err.span_help(span_data.span(), help);
597 extra_span = true;
598 } else {
599 err.help(help);
600 }
601 }
602
603 let mut backtrace_title = String::from("BACKTRACE");
605 if extra_span {
606 write!(backtrace_title, " (of the first span)").unwrap();
607 }
608 if let Some(thread) = thread {
609 let thread_name = machine.threads.get_thread_display_name(thread);
610 if thread_name != "main" {
611 write!(backtrace_title, " on thread `{thread_name}`").unwrap();
613 };
614 }
615 write!(backtrace_title, ":").unwrap();
616 err.note(backtrace_title);
617 for (idx, frame_info) in stacktrace.iter().enumerate() {
618 let is_local = machine.is_local(frame_info);
619 if is_local && idx > 0 {
621 err.subdiagnostic(frame_info.as_note(machine.tcx));
622 } else {
623 let sm = sess.source_map();
624 let span = sm.span_to_embeddable_string(frame_info.span);
625 err.note(format!("{frame_info} at {span}"));
626 }
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 | CreatedAlloc(..)
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 CreatedAlloc(AllocId(id), size, align, kind) =>
669 format!(
670 "created {kind} allocation of {size} bytes (alignment {align} bytes) with id {id}",
671 size = size.bytes(),
672 align = align.bytes(),
673 ),
674 AccessedAlloc(AllocId(id), access_kind) =>
675 format!("{access_kind} to allocation with id {id}"),
676 FreedAlloc(AllocId(id)) => format!("freed allocation with id {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}