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 GenmcStuckExecution,
36 MultipleSymbolDefinitions {
37 link_name: Symbol,
38 first: SpanData,
39 first_crate: Symbol,
40 second: SpanData,
41 second_crate: Symbol,
42 },
43 SymbolShimClashing {
44 link_name: Symbol,
45 span: SpanData,
46 },
47 DataRace {
48 involves_non_atomic: bool,
49 ptr: interpret::Pointer<AllocId>,
50 op1: RacingOp,
51 op2: RacingOp,
52 extra: Option<&'static str>,
53 retag_explain: bool,
54 },
55 UnsupportedForeignItem(String),
56}
57
58pub struct RacingOp {
59 pub action: String,
60 pub thread_info: String,
61 pub span: SpanData,
62}
63
64impl fmt::Display for TerminationInfo {
65 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
66 use TerminationInfo::*;
67 match self {
68 Exit { code, .. } => write!(f, "the evaluated program completed with exit code {code}"),
69 Abort(msg) => write!(f, "{msg}"),
70 Interrupted => write!(f, "interpretation was interrupted"),
71 UnsupportedInIsolation(msg) => write!(f, "{msg}"),
72 Int2PtrWithStrictProvenance =>
73 write!(
74 f,
75 "integer-to-pointer casts and `ptr::with_exposed_provenance` are not supported with `-Zmiri-strict-provenance`"
76 ),
77 StackedBorrowsUb { msg, .. } => write!(f, "{msg}"),
78 TreeBorrowsUb { title, .. } => write!(f, "{title}"),
79 Deadlock => write!(f, "the evaluated program deadlocked"),
80 GenmcStuckExecution => write!(f, "GenMC determined that the execution got stuck"),
81 MultipleSymbolDefinitions { link_name, .. } =>
82 write!(f, "multiple definitions of symbol `{link_name}`"),
83 SymbolShimClashing { link_name, .. } =>
84 write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
85 DataRace { involves_non_atomic, ptr, op1, op2, .. } =>
86 write!(
87 f,
88 "{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}",
89 if *involves_non_atomic { "Data race" } else { "Race condition" },
90 op1.action,
91 op1.thread_info,
92 op2.action,
93 op2.thread_info
94 ),
95 UnsupportedForeignItem(msg) => write!(f, "{msg}"),
96 }
97 }
98}
99
100impl fmt::Debug for TerminationInfo {
101 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
102 write!(f, "{self}")
103 }
104}
105
106impl MachineStopType for TerminationInfo {
107 fn diagnostic_message(&self) -> DiagMessage {
108 self.to_string().into()
109 }
110 fn add_args(
111 self: Box<Self>,
112 _: &mut dyn FnMut(std::borrow::Cow<'static, str>, rustc_errors::DiagArgValue),
113 ) {
114 }
115}
116
117pub enum NonHaltingDiagnostic {
119 CreatedPointerTag(NonZero<u64>, Option<String>, Option<(AllocId, AllocRange, ProvenanceExtra)>),
123 PoppedPointerTag(Item, String),
125 CreatedAlloc(AllocId, Size, Align, MemoryKind),
126 FreedAlloc(AllocId),
127 AccessedAlloc(AllocId, AccessKind),
128 RejectedIsolatedOp(String),
129 ProgressReport {
130 block_count: u64, },
132 Int2Ptr {
133 details: bool,
134 },
135 NativeCallSharedMem,
136 WeakMemoryOutdatedLoad {
137 ptr: Pointer,
138 },
139 ExternTypeReborrow,
140}
141
142pub enum DiagLevel {
144 Error,
145 Warning,
146 Note,
147}
148
149macro_rules! note {
151 ($($tt:tt)*) => { (None, format!($($tt)*)) };
152}
153macro_rules! note_span {
155 ($span:expr, $($tt:tt)*) => { (Some($span), format!($($tt)*)) };
156}
157
158pub fn prune_stacktrace<'tcx>(
162 mut stacktrace: Vec<FrameInfo<'tcx>>,
163 machine: &MiriMachine<'tcx>,
164) -> (Vec<FrameInfo<'tcx>>, bool) {
165 match machine.backtrace_style {
166 BacktraceStyle::Off => {
167 stacktrace.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
170 stacktrace.truncate(1);
172 (stacktrace, false)
173 }
174 BacktraceStyle::Short => {
175 let original_len = stacktrace.len();
176 let has_local_frame = stacktrace.iter().any(|frame| machine.is_local(frame));
180 if has_local_frame {
181 stacktrace
184 .retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
185
186 stacktrace = stacktrace
191 .into_iter()
192 .take_while(|frame| {
193 let def_id = frame.instance.def_id();
194 let path = machine.tcx.def_path_str(def_id);
195 !path.contains("__rust_begin_short_backtrace")
196 })
197 .collect::<Vec<_>>();
198
199 while stacktrace.len() > 1
205 && stacktrace.last().is_some_and(|frame| !machine.is_local(frame))
206 {
207 stacktrace.pop();
208 }
209 }
210 let was_pruned = stacktrace.len() != original_len;
211 (stacktrace, was_pruned)
212 }
213 BacktraceStyle::Full => (stacktrace, false),
214 }
215}
216
217pub fn report_error<'tcx>(
221 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
222 e: InterpErrorInfo<'tcx>,
223) -> Option<(i32, bool)> {
224 use InterpErrorKind::*;
225 use UndefinedBehaviorInfo::*;
226
227 let mut labels = vec![];
228
229 let (title, helps) = if let MachineStop(info) = e.kind() {
230 let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
231 use TerminationInfo::*;
232 let title = match info {
233 &Exit { code, leak_check } => return Some((code, leak_check)),
234 Abort(_) => Some("abnormal termination"),
235 Interrupted => None,
236 UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance | UnsupportedForeignItem(_) =>
237 Some("unsupported operation"),
238 StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
239 Some("Undefined Behavior"),
240 Deadlock => {
241 labels.push(format!("this thread got stuck here"));
242 None
243 }
244 GenmcStuckExecution => {
245 assert!(ecx.machine.data_race.as_genmc_ref().is_some());
247 tracing::info!("GenMC: found stuck execution");
248 return Some((0, true));
249 }
250 MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
251 };
252 #[rustfmt::skip]
253 let helps = match info {
254 UnsupportedInIsolation(_) =>
255 vec![
256 note!("set `MIRIFLAGS=-Zmiri-disable-isolation` to disable isolation;"),
257 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"),
258 ],
259 UnsupportedForeignItem(_) => {
260 vec![
261 note!("this means the program tried to do something Miri does not support; it does not indicate a bug in the program"),
262 ]
263 }
264 StackedBorrowsUb { help, history, .. } => {
265 labels.extend(help.clone());
266 let mut helps = vec![
267 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental"),
268 note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information"),
269 ];
270 if let Some(TagHistory {created, invalidated, protected}) = history.clone() {
271 helps.push((Some(created.1), created.0));
272 if let Some((msg, span)) = invalidated {
273 helps.push(note_span!(span, "{msg}"));
274 }
275 if let Some((protector_msg, protector_span)) = protected {
276 helps.push(note_span!(protector_span, "{protector_msg}"));
277 }
278 }
279 helps
280 },
281 TreeBorrowsUb { title: _, details, history } => {
282 let mut helps = vec![
283 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")
284 ];
285 for m in details {
286 helps.push(note!("{m}"));
287 }
288 for event in history.events.clone() {
289 helps.push(event);
290 }
291 helps
292 }
293 MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
294 vec![
295 note_span!(*first, "it's first defined here, in crate `{first_crate}`"),
296 note_span!(*second, "then it's defined here again, in crate `{second_crate}`"),
297 ],
298 SymbolShimClashing { link_name, span } =>
299 vec![note_span!(*span, "the `{link_name}` symbol is defined here")],
300 Int2PtrWithStrictProvenance =>
301 vec![note!("use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead")],
302 DataRace { op1, extra, retag_explain, .. } => {
303 labels.push(format!("(2) just happened here"));
304 let mut helps = vec![note_span!(op1.span, "and (1) occurred earlier here")];
305 if let Some(extra) = extra {
306 helps.push(note!("{extra}"));
307 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"));
308 }
309 if *retag_explain {
310 helps.push(note!("retags occur on all (re)borrows and as well as when references are copied or moved"));
311 helps.push(note!("retags permit optimizations that insert speculative reads or writes"));
312 helps.push(note!("therefore from the perspective of data races, a retag has the same implications as a read or write"));
313 }
314 helps.push(note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"));
315 helps.push(note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"));
316 helps
317 }
318 ,
319 _ => vec![],
320 };
321 (title, helps)
322 } else {
323 let title = match e.kind() {
324 UndefinedBehavior(ValidationError(validation_err))
325 if matches!(
326 validation_err.kind,
327 ValidationErrorKind::PointerAsInt { .. } | ValidationErrorKind::PartialPointer
328 ) =>
329 {
330 ecx.handle_ice(); bug!(
332 "This validation error should be impossible in Miri: {}",
333 format_interp_error(ecx.tcx.dcx(), e)
334 );
335 }
336 UndefinedBehavior(_) => "Undefined Behavior",
337 ResourceExhaustion(_) => "resource exhaustion",
338 Unsupported(
339 UnsupportedOpInfo::Unsupported(_)
341 | UnsupportedOpInfo::UnsizedLocal
342 | UnsupportedOpInfo::ExternTypeField,
343 ) => "unsupported operation",
344 InvalidProgram(
345 InvalidProgramInfo::AlreadyReported(_) | InvalidProgramInfo::Layout(..),
347 ) => "post-monomorphization error",
348 _ => {
349 ecx.handle_ice(); bug!(
351 "This error should be impossible in Miri: {}",
352 format_interp_error(ecx.tcx.dcx(), e)
353 );
354 }
355 };
356 #[rustfmt::skip]
357 let helps = match e.kind() {
358 Unsupported(_) =>
359 vec![
360 note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
361 ],
362 UndefinedBehavior(AlignmentCheckFailed { .. })
363 if ecx.machine.check_alignment == AlignmentCheck::Symbolic
364 =>
365 vec![
366 note!("this usually indicates that your program performed an invalid operation and caused Undefined Behavior"),
367 note!("but due to `-Zmiri-symbolic-alignment-check`, alignment errors can also be false positives"),
368 ],
369 UndefinedBehavior(info) => {
370 let mut helps = vec![
371 note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"),
372 note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"),
373 ];
374 match info {
375 PointerUseAfterFree(alloc_id, _) | PointerOutOfBounds { alloc_id, .. } => {
376 if let Some(span) = ecx.machine.allocated_span(*alloc_id) {
377 helps.push(note_span!(span, "{:?} was allocated here:", alloc_id));
378 }
379 if let Some(span) = ecx.machine.deallocated_span(*alloc_id) {
380 helps.push(note_span!(span, "{:?} was deallocated here:", alloc_id));
381 }
382 }
383 AbiMismatchArgument { .. } | AbiMismatchReturn { .. } => {
384 helps.push(note!("this means these two types are not *guaranteed* to be ABI-compatible across all targets"));
385 helps.push(note!("if you think this code should be accepted anyway, please report an issue with Miri"));
386 }
387 _ => {},
388 }
389 helps
390 }
391 InvalidProgram(
392 InvalidProgramInfo::AlreadyReported(_)
393 ) => {
394 return None;
396 }
397 _ =>
398 vec![],
399 };
400 (Some(title), helps)
401 };
402
403 let stacktrace = ecx.generate_stacktrace();
404 let (stacktrace, mut any_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
405
406 let mut show_all_threads = false;
407
408 let mut extra = String::new();
411 match e.kind() {
412 UndefinedBehavior(InvalidUninitBytes(Some((alloc_id, access)))) => {
413 writeln!(
414 extra,
415 "Uninitialized memory occurred at {alloc_id:?}{range:?}, in this allocation:",
416 range = access.bad,
417 )
418 .unwrap();
419 writeln!(extra, "{:?}", ecx.dump_alloc(*alloc_id)).unwrap();
420 }
421 MachineStop(info) => {
422 let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
423 match info {
424 TerminationInfo::Deadlock => {
425 show_all_threads = true;
426 }
427 _ => {}
428 }
429 }
430 _ => {}
431 }
432
433 let mut primary_msg = String::new();
434 if let Some(title) = title {
435 write!(primary_msg, "{title}: ").unwrap();
436 }
437 write!(primary_msg, "{}", format_interp_error(ecx.tcx.dcx(), e)).unwrap();
438
439 if labels.is_empty() {
440 labels.push(format!("{} occurred here", title.unwrap_or("error")));
441 }
442
443 report_msg(
444 DiagLevel::Error,
445 primary_msg,
446 labels,
447 vec![],
448 helps,
449 &stacktrace,
450 Some(ecx.active_thread()),
451 &ecx.machine,
452 );
453
454 eprint!("{extra}"); if show_all_threads {
457 for (thread, stack) in ecx.machine.threads.all_stacks() {
458 if thread != ecx.active_thread() {
459 let stacktrace = Frame::generate_stacktrace_from_stack(stack);
460 let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
461 any_pruned |= was_pruned;
462 report_msg(
463 DiagLevel::Error,
464 format!("the evaluated program deadlocked"),
465 vec![format!("this thread got stuck here")],
466 vec![],
467 vec![],
468 &stacktrace,
469 Some(thread),
470 &ecx.machine,
471 )
472 }
473 }
474 }
475
476 if any_pruned {
478 ecx.tcx.dcx().note(
479 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
480 );
481 }
482
483 for (i, frame) in ecx.active_thread_stack().iter().enumerate() {
485 trace!("-------------------");
486 trace!("Frame {}", i);
487 trace!(" return: {:?}", frame.return_place);
488 for (i, local) in frame.locals.iter().enumerate() {
489 trace!(" local {}: {:?}", i, local);
490 }
491 }
492
493 None
494}
495
496pub fn report_leaks<'tcx>(
497 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
498 leaks: Vec<(AllocId, MemoryKind, Allocation<Provenance, AllocExtra<'tcx>, MiriAllocBytes>)>,
499) {
500 let mut any_pruned = false;
501 for (id, kind, alloc) in leaks {
502 let mut title = format!(
503 "memory leaked: {id:?} ({}, size: {:?}, align: {:?})",
504 kind,
505 alloc.size().bytes(),
506 alloc.align.bytes()
507 );
508 let Some(backtrace) = alloc.extra.backtrace else {
509 ecx.tcx.dcx().err(title);
510 continue;
511 };
512 title.push_str(", allocated here:");
513 let (backtrace, pruned) = prune_stacktrace(backtrace, &ecx.machine);
514 any_pruned |= pruned;
515 report_msg(
516 DiagLevel::Error,
517 title,
518 vec![],
519 vec![],
520 vec![],
521 &backtrace,
522 None, &ecx.machine,
524 );
525 }
526 if any_pruned {
527 ecx.tcx.dcx().note(
528 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
529 );
530 }
531}
532
533pub fn report_msg<'tcx>(
539 diag_level: DiagLevel,
540 title: String,
541 span_msg: Vec<String>,
542 notes: Vec<(Option<SpanData>, String)>,
543 helps: Vec<(Option<SpanData>, String)>,
544 stacktrace: &[FrameInfo<'tcx>],
545 thread: Option<ThreadId>,
546 machine: &MiriMachine<'tcx>,
547) {
548 let span = stacktrace.first().map_or(DUMMY_SP, |fi| fi.span);
549 let sess = machine.tcx.sess;
550 let level = match diag_level {
551 DiagLevel::Error => Level::Error,
552 DiagLevel::Warning => Level::Warning,
553 DiagLevel::Note => Level::Note,
554 };
555 let mut err = Diag::<()>::new(sess.dcx(), level, title);
556 err.span(span);
557
558 if span != DUMMY_SP {
560 for line in span_msg {
561 err.span_label(span, line);
562 }
563 } else {
564 for line in span_msg {
566 err.note(line);
567 }
568 err.note("(no span available)");
569 }
570
571 let mut extra_span = false;
573 for (span_data, note) in notes {
574 if let Some(span_data) = span_data {
575 err.span_note(span_data.span(), note);
576 extra_span = true;
577 } else {
578 err.note(note);
579 }
580 }
581 for (span_data, help) in helps {
582 if let Some(span_data) = span_data {
583 err.span_help(span_data.span(), help);
584 extra_span = true;
585 } else {
586 err.help(help);
587 }
588 }
589
590 let mut backtrace_title = String::from("BACKTRACE");
592 if extra_span {
593 write!(backtrace_title, " (of the first span)").unwrap();
594 }
595 if let Some(thread) = thread {
596 let thread_name = machine.threads.get_thread_display_name(thread);
597 if thread_name != "main" {
598 write!(backtrace_title, " on thread `{thread_name}`").unwrap();
600 };
601 }
602 write!(backtrace_title, ":").unwrap();
603 err.note(backtrace_title);
604 for (idx, frame_info) in stacktrace.iter().enumerate() {
605 let is_local = machine.is_local(frame_info);
606 if is_local && idx > 0 {
608 err.subdiagnostic(frame_info.as_note(machine.tcx));
609 } else {
610 let sm = sess.source_map();
611 let span = sm.span_to_embeddable_string(frame_info.span);
612 err.note(format!("{frame_info} at {span}"));
613 }
614 }
615
616 err.emit();
617}
618
619impl<'tcx> MiriMachine<'tcx> {
620 pub fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
621 use NonHaltingDiagnostic::*;
622
623 let stacktrace = Frame::generate_stacktrace_from_stack(self.threads.active_thread_stack());
624 let (stacktrace, _was_pruned) = prune_stacktrace(stacktrace, self);
625
626 let (label, diag_level) = match &e {
627 RejectedIsolatedOp(_) =>
628 ("operation rejected by isolation".to_string(), DiagLevel::Warning),
629 Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning),
630 NativeCallSharedMem =>
631 ("sharing memory with a native function".to_string(), DiagLevel::Warning),
632 ExternTypeReborrow =>
633 ("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
634 CreatedPointerTag(..)
635 | PoppedPointerTag(..)
636 | CreatedAlloc(..)
637 | AccessedAlloc(..)
638 | FreedAlloc(..)
639 | ProgressReport { .. }
640 | WeakMemoryOutdatedLoad { .. } =>
641 ("tracking was triggered here".to_string(), DiagLevel::Note),
642 };
643
644 let title = match &e {
645 CreatedPointerTag(tag, None, _) => format!("created base tag {tag:?}"),
646 CreatedPointerTag(tag, Some(perm), None) =>
647 format!("created {tag:?} with {perm} derived from unknown tag"),
648 CreatedPointerTag(tag, Some(perm), Some((alloc_id, range, orig_tag))) =>
649 format!(
650 "created tag {tag:?} with {perm} at {alloc_id:?}{range:?} derived from {orig_tag:?}"
651 ),
652 PoppedPointerTag(item, cause) => format!("popped tracked tag for item {item:?}{cause}"),
653 CreatedAlloc(AllocId(id), size, align, kind) =>
654 format!(
655 "created {kind} allocation of {size} bytes (alignment {align} bytes) with id {id}",
656 size = size.bytes(),
657 align = align.bytes(),
658 ),
659 AccessedAlloc(AllocId(id), access_kind) =>
660 format!("{access_kind} to allocation with id {id}"),
661 FreedAlloc(AllocId(id)) => format!("freed allocation with id {id}"),
662 RejectedIsolatedOp(op) => format!("{op} was made to return an error due to isolation"),
663 ProgressReport { .. } =>
664 format!("progress report: current operation being executed is here"),
665 Int2Ptr { .. } => format!("integer-to-pointer cast"),
666 NativeCallSharedMem => format!("sharing memory with a native function called via FFI"),
667 WeakMemoryOutdatedLoad { ptr } =>
668 format!("weak memory emulation: outdated value returned from load at {ptr}"),
669 ExternTypeReborrow =>
670 format!("reborrow of a reference to `extern type` is not properly supported"),
671 };
672
673 let notes = match &e {
674 ProgressReport { block_count } => {
675 vec![note!("so far, {block_count} basic blocks have been executed")]
676 }
677 _ => vec![],
678 };
679
680 let helps = match &e {
681 Int2Ptr { details: true } => {
682 let mut v = vec![
683 note!(
684 "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"
685 ),
686 note!(
687 "see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation"
688 ),
689 note!(
690 "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"
691 ),
692 note!(
693 "you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics"
694 ),
695 ];
696 if self.borrow_tracker.as_ref().is_some_and(|b| {
697 matches!(
698 b.borrow().borrow_tracker_method(),
699 BorrowTrackerMethod::TreeBorrows { .. }
700 )
701 }) {
702 v.push(
703 note!("Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used")
704 );
705 } else {
706 v.push(
707 note!("alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning")
708 );
709 }
710 v
711 }
712 NativeCallSharedMem => {
713 vec![
714 note!(
715 "when memory is shared with a native function call, Miri stops tracking initialization and provenance for that memory"
716 ),
717 note!(
718 "in particular, Miri assumes that the native call initializes all memory it has access to"
719 ),
720 note!(
721 "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory"
722 ),
723 note!(
724 "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"
725 ),
726 ]
727 }
728 ExternTypeReborrow => {
729 assert!(self.borrow_tracker.as_ref().is_some_and(|b| {
730 matches!(
731 b.borrow().borrow_tracker_method(),
732 BorrowTrackerMethod::StackedBorrows
733 )
734 }));
735 vec![
736 note!(
737 "`extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code"
738 ),
739 note!(
740 "try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead"
741 ),
742 ]
743 }
744 _ => vec![],
745 };
746
747 report_msg(
748 diag_level,
749 title,
750 vec![label],
751 notes,
752 helps,
753 &stacktrace,
754 Some(self.threads.active_thread()),
755 self,
756 );
757 }
758}
759
760impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
761pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
762 fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
763 let this = self.eval_context_ref();
764 this.machine.emit_diagnostic(e);
765 }
766
767 fn handle_ice(&self) {
769 eprintln!();
770 eprintln!(
771 "Miri caused an ICE during evaluation. Here's the interpreter backtrace at the time of the panic:"
772 );
773 let this = self.eval_context_ref();
774 let stacktrace = this.generate_stacktrace();
775 report_msg(
776 DiagLevel::Note,
777 "the place in the program where the ICE was triggered".to_string(),
778 vec![],
779 vec![],
780 vec![],
781 &stacktrace,
782 Some(this.active_thread()),
783 &this.machine,
784 );
785 }
786}