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:?}. (2) just happened here",
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 msg = 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 => Some("deadlock"),
241 GenmcStuckExecution => {
242 assert!(ecx.machine.data_race.as_genmc_ref().is_some());
244 tracing::info!("GenMC: found stuck execution");
245 return Some((0, true));
246 }
247 MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
248 };
249 #[rustfmt::skip]
250 let helps = match info {
251 UnsupportedInIsolation(_) =>
252 vec![
253 note!("set `MIRIFLAGS=-Zmiri-disable-isolation` to disable isolation;"),
254 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"),
255 ],
256 UnsupportedForeignItem(_) => {
257 vec![
258 note!("if this is a basic API commonly used on this target, please report an issue with Miri"),
259 note!("however, note that Miri does not aim to support every FFI function out there; for instance, we will not support APIs for things such as GUIs, scripting languages, or databases"),
260 ]
261 }
262 StackedBorrowsUb { help, history, .. } => {
263 msg.extend(help.clone());
264 let mut helps = vec![
265 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental"),
266 note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information"),
267 ];
268 if let Some(TagHistory {created, invalidated, protected}) = history.clone() {
269 helps.push((Some(created.1), created.0));
270 if let Some((msg, span)) = invalidated {
271 helps.push(note_span!(span, "{msg}"));
272 }
273 if let Some((protector_msg, protector_span)) = protected {
274 helps.push(note_span!(protector_span, "{protector_msg}"));
275 }
276 }
277 helps
278 },
279 TreeBorrowsUb { title: _, details, history } => {
280 let mut helps = vec![
281 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")
282 ];
283 for m in details {
284 helps.push(note!("{m}"));
285 }
286 for event in history.events.clone() {
287 helps.push(event);
288 }
289 helps
290 }
291 MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
292 vec![
293 note_span!(*first, "it's first defined here, in crate `{first_crate}`"),
294 note_span!(*second, "then it's defined here again, in crate `{second_crate}`"),
295 ],
296 SymbolShimClashing { link_name, span } =>
297 vec![note_span!(*span, "the `{link_name}` symbol is defined here")],
298 Int2PtrWithStrictProvenance =>
299 vec![note!("use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead")],
300 DataRace { op1, extra, retag_explain, .. } => {
301 let mut helps = vec![note_span!(op1.span, "and (1) occurred earlier here")];
302 if let Some(extra) = extra {
303 helps.push(note!("{extra}"));
304 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"));
305 }
306 if *retag_explain {
307 helps.push(note!("retags occur on all (re)borrows and as well as when references are copied or moved"));
308 helps.push(note!("retags permit optimizations that insert speculative reads or writes"));
309 helps.push(note!("therefore from the perspective of data races, a retag has the same implications as a read or write"));
310 }
311 helps.push(note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"));
312 helps.push(note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"));
313 helps
314 }
315 ,
316 _ => vec![],
317 };
318 (title, helps)
319 } else {
320 let title = match e.kind() {
321 UndefinedBehavior(ValidationError(validation_err))
322 if matches!(
323 validation_err.kind,
324 ValidationErrorKind::PointerAsInt { .. } | ValidationErrorKind::PartialPointer
325 ) =>
326 {
327 ecx.handle_ice(); bug!(
329 "This validation error should be impossible in Miri: {}",
330 format_interp_error(ecx.tcx.dcx(), e)
331 );
332 }
333 UndefinedBehavior(_) => "Undefined Behavior",
334 ResourceExhaustion(_) => "resource exhaustion",
335 Unsupported(
336 UnsupportedOpInfo::Unsupported(_)
338 | UnsupportedOpInfo::UnsizedLocal
339 | UnsupportedOpInfo::ExternTypeField,
340 ) => "unsupported operation",
341 InvalidProgram(
342 InvalidProgramInfo::AlreadyReported(_) | InvalidProgramInfo::Layout(..),
344 ) => "post-monomorphization error",
345 _ => {
346 ecx.handle_ice(); bug!(
348 "This error should be impossible in Miri: {}",
349 format_interp_error(ecx.tcx.dcx(), e)
350 );
351 }
352 };
353 #[rustfmt::skip]
354 let helps = match e.kind() {
355 Unsupported(_) =>
356 vec![
357 note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
358 ],
359 UndefinedBehavior(AlignmentCheckFailed { .. })
360 if ecx.machine.check_alignment == AlignmentCheck::Symbolic
361 =>
362 vec![
363 note!("this usually indicates that your program performed an invalid operation and caused Undefined Behavior"),
364 note!("but due to `-Zmiri-symbolic-alignment-check`, alignment errors can also be false positives"),
365 ],
366 UndefinedBehavior(info) => {
367 let mut helps = vec![
368 note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"),
369 note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"),
370 ];
371 match info {
372 PointerUseAfterFree(alloc_id, _) | PointerOutOfBounds { alloc_id, .. } => {
373 if let Some(span) = ecx.machine.allocated_span(*alloc_id) {
374 helps.push(note_span!(span, "{:?} was allocated here:", alloc_id));
375 }
376 if let Some(span) = ecx.machine.deallocated_span(*alloc_id) {
377 helps.push(note_span!(span, "{:?} was deallocated here:", alloc_id));
378 }
379 }
380 AbiMismatchArgument { .. } | AbiMismatchReturn { .. } => {
381 helps.push(note!("this means these two types are not *guaranteed* to be ABI-compatible across all targets"));
382 helps.push(note!("if you think this code should be accepted anyway, please report an issue with Miri"));
383 }
384 _ => {},
385 }
386 helps
387 }
388 InvalidProgram(
389 InvalidProgramInfo::AlreadyReported(_)
390 ) => {
391 return None;
393 }
394 _ =>
395 vec![],
396 };
397 (Some(title), helps)
398 };
399
400 let stacktrace = ecx.generate_stacktrace();
401 let (stacktrace, mut any_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
402
403 let mut show_all_threads = false;
404
405 let mut extra = String::new();
408 match e.kind() {
409 UndefinedBehavior(InvalidUninitBytes(Some((alloc_id, access)))) => {
410 writeln!(
411 extra,
412 "Uninitialized memory occurred at {alloc_id:?}{range:?}, in this allocation:",
413 range = access.bad,
414 )
415 .unwrap();
416 writeln!(extra, "{:?}", ecx.dump_alloc(*alloc_id)).unwrap();
417 }
418 MachineStop(info) => {
419 let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
420 match info {
421 TerminationInfo::Deadlock => {
422 show_all_threads = true;
423 }
424 _ => {}
425 }
426 }
427 _ => {}
428 }
429
430 msg.insert(0, format_interp_error(ecx.tcx.dcx(), e));
431
432 report_msg(
433 DiagLevel::Error,
434 if let Some(title) = title { format!("{title}: {}", msg[0]) } else { msg[0].clone() },
435 msg,
436 vec![],
437 helps,
438 &stacktrace,
439 Some(ecx.active_thread()),
440 &ecx.machine,
441 );
442
443 eprint!("{extra}"); if show_all_threads {
446 for (thread, stack) in ecx.machine.threads.all_stacks() {
447 if thread != ecx.active_thread() {
448 let stacktrace = Frame::generate_stacktrace_from_stack(stack);
449 let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
450 any_pruned |= was_pruned;
451 report_msg(
452 DiagLevel::Error,
453 format!("deadlock: the evaluated program deadlocked"),
454 vec![format!("the evaluated program deadlocked")],
455 vec![],
456 vec![],
457 &stacktrace,
458 Some(thread),
459 &ecx.machine,
460 )
461 }
462 }
463 }
464
465 if any_pruned {
467 ecx.tcx.dcx().note(
468 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
469 );
470 }
471
472 for (i, frame) in ecx.active_thread_stack().iter().enumerate() {
474 trace!("-------------------");
475 trace!("Frame {}", i);
476 trace!(" return: {:?}", frame.return_place);
477 for (i, local) in frame.locals.iter().enumerate() {
478 trace!(" local {}: {:?}", i, local);
479 }
480 }
481
482 None
483}
484
485pub fn report_leaks<'tcx>(
486 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
487 leaks: Vec<(AllocId, MemoryKind, Allocation<Provenance, AllocExtra<'tcx>, MiriAllocBytes>)>,
488) {
489 let mut any_pruned = false;
490 for (id, kind, alloc) in leaks {
491 let mut title = format!(
492 "memory leaked: {id:?} ({}, size: {:?}, align: {:?})",
493 kind,
494 alloc.size().bytes(),
495 alloc.align.bytes()
496 );
497 let Some(backtrace) = alloc.extra.backtrace else {
498 ecx.tcx.dcx().err(title);
499 continue;
500 };
501 title.push_str(", allocated here:");
502 let (backtrace, pruned) = prune_stacktrace(backtrace, &ecx.machine);
503 any_pruned |= pruned;
504 report_msg(
505 DiagLevel::Error,
506 title,
507 vec![],
508 vec![],
509 vec![],
510 &backtrace,
511 None, &ecx.machine,
513 );
514 }
515 if any_pruned {
516 ecx.tcx.dcx().note(
517 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
518 );
519 }
520}
521
522pub fn report_msg<'tcx>(
528 diag_level: DiagLevel,
529 title: String,
530 span_msg: Vec<String>,
531 notes: Vec<(Option<SpanData>, String)>,
532 helps: Vec<(Option<SpanData>, String)>,
533 stacktrace: &[FrameInfo<'tcx>],
534 thread: Option<ThreadId>,
535 machine: &MiriMachine<'tcx>,
536) {
537 let span = stacktrace.first().map_or(DUMMY_SP, |fi| fi.span);
538 let sess = machine.tcx.sess;
539 let level = match diag_level {
540 DiagLevel::Error => Level::Error,
541 DiagLevel::Warning => Level::Warning,
542 DiagLevel::Note => Level::Note,
543 };
544 let mut err = Diag::<()>::new(sess.dcx(), level, title);
545 err.span(span);
546
547 if span != DUMMY_SP {
549 for line in span_msg {
550 err.span_label(span, line);
551 }
552 } else {
553 for line in span_msg {
555 err.note(line);
556 }
557 err.note("(no span available)");
558 }
559
560 let mut extra_span = false;
562 for (span_data, note) in notes {
563 if let Some(span_data) = span_data {
564 err.span_note(span_data.span(), note);
565 extra_span = true;
566 } else {
567 err.note(note);
568 }
569 }
570 for (span_data, help) in helps {
571 if let Some(span_data) = span_data {
572 err.span_help(span_data.span(), help);
573 extra_span = true;
574 } else {
575 err.help(help);
576 }
577 }
578
579 let mut backtrace_title = String::from("BACKTRACE");
581 if extra_span {
582 write!(backtrace_title, " (of the first span)").unwrap();
583 }
584 if let Some(thread) = thread {
585 let thread_name = machine.threads.get_thread_display_name(thread);
586 if thread_name != "main" {
587 write!(backtrace_title, " on thread `{thread_name}`").unwrap();
589 };
590 }
591 write!(backtrace_title, ":").unwrap();
592 err.note(backtrace_title);
593 for (idx, frame_info) in stacktrace.iter().enumerate() {
594 let is_local = machine.is_local(frame_info);
595 if is_local && idx > 0 {
597 err.subdiagnostic(frame_info.as_note(machine.tcx));
598 } else {
599 let sm = sess.source_map();
600 let span = sm.span_to_embeddable_string(frame_info.span);
601 err.note(format!("{frame_info} at {span}"));
602 }
603 }
604
605 err.emit();
606}
607
608impl<'tcx> MiriMachine<'tcx> {
609 pub fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
610 use NonHaltingDiagnostic::*;
611
612 let stacktrace = Frame::generate_stacktrace_from_stack(self.threads.active_thread_stack());
613 let (stacktrace, _was_pruned) = prune_stacktrace(stacktrace, self);
614
615 let (title, diag_level) = match &e {
616 RejectedIsolatedOp(_) =>
617 ("operation rejected by isolation".to_string(), DiagLevel::Warning),
618 Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning),
619 NativeCallSharedMem =>
620 ("sharing memory with a native function".to_string(), DiagLevel::Warning),
621 ExternTypeReborrow =>
622 ("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
623 CreatedPointerTag(..)
624 | PoppedPointerTag(..)
625 | CreatedAlloc(..)
626 | AccessedAlloc(..)
627 | FreedAlloc(..)
628 | ProgressReport { .. }
629 | WeakMemoryOutdatedLoad { .. } =>
630 ("tracking was triggered".to_string(), DiagLevel::Note),
631 };
632
633 let msg = match &e {
634 CreatedPointerTag(tag, None, _) => format!("created base tag {tag:?}"),
635 CreatedPointerTag(tag, Some(perm), None) =>
636 format!("created {tag:?} with {perm} derived from unknown tag"),
637 CreatedPointerTag(tag, Some(perm), Some((alloc_id, range, orig_tag))) =>
638 format!(
639 "created tag {tag:?} with {perm} at {alloc_id:?}{range:?} derived from {orig_tag:?}"
640 ),
641 PoppedPointerTag(item, cause) => format!("popped tracked tag for item {item:?}{cause}"),
642 CreatedAlloc(AllocId(id), size, align, kind) =>
643 format!(
644 "created {kind} allocation of {size} bytes (alignment {align} bytes) with id {id}",
645 size = size.bytes(),
646 align = align.bytes(),
647 ),
648 AccessedAlloc(AllocId(id), access_kind) =>
649 format!("{access_kind} to allocation with id {id}"),
650 FreedAlloc(AllocId(id)) => format!("freed allocation with id {id}"),
651 RejectedIsolatedOp(op) => format!("{op} was made to return an error due to isolation"),
652 ProgressReport { .. } =>
653 format!("progress report: current operation being executed is here"),
654 Int2Ptr { .. } => format!("integer-to-pointer cast"),
655 NativeCallSharedMem => format!("sharing memory with a native function called via FFI"),
656 WeakMemoryOutdatedLoad { ptr } =>
657 format!("weak memory emulation: outdated value returned from load at {ptr}"),
658 ExternTypeReborrow =>
659 format!("reborrow of a reference to `extern type` is not properly supported"),
660 };
661
662 let notes = match &e {
663 ProgressReport { block_count } => {
664 vec![note!("so far, {block_count} basic blocks have been executed")]
665 }
666 _ => vec![],
667 };
668
669 let helps = match &e {
670 Int2Ptr { details: true } => {
671 let mut v = vec![
672 note!(
673 "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"
674 ),
675 note!(
676 "see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation"
677 ),
678 note!(
679 "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"
680 ),
681 note!(
682 "you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics"
683 ),
684 ];
685 if self.borrow_tracker.as_ref().is_some_and(|b| {
686 matches!(b.borrow().borrow_tracker_method(), BorrowTrackerMethod::TreeBorrows)
687 }) {
688 v.push(
689 note!("Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used")
690 );
691 } else {
692 v.push(
693 note!("alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning")
694 );
695 }
696 v
697 }
698 NativeCallSharedMem => {
699 vec![
700 note!(
701 "when memory is shared with a native function call, Miri stops tracking initialization and provenance for that memory"
702 ),
703 note!(
704 "in particular, Miri assumes that the native call initializes all memory it has access to"
705 ),
706 note!(
707 "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory"
708 ),
709 note!(
710 "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"
711 ),
712 ]
713 }
714 ExternTypeReborrow => {
715 assert!(self.borrow_tracker.as_ref().is_some_and(|b| {
716 matches!(
717 b.borrow().borrow_tracker_method(),
718 BorrowTrackerMethod::StackedBorrows
719 )
720 }));
721 vec![
722 note!(
723 "`extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code"
724 ),
725 note!(
726 "try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead"
727 ),
728 ]
729 }
730 _ => vec![],
731 };
732
733 report_msg(
734 diag_level,
735 title,
736 vec![msg],
737 notes,
738 helps,
739 &stacktrace,
740 Some(self.threads.active_thread()),
741 self,
742 );
743 }
744}
745
746impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
747pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
748 fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
749 let this = self.eval_context_ref();
750 this.machine.emit_diagnostic(e);
751 }
752
753 fn handle_ice(&self) {
755 eprintln!();
756 eprintln!(
757 "Miri caused an ICE during evaluation. Here's the interpreter backtrace at the time of the panic:"
758 );
759 let this = self.eval_context_ref();
760 let stacktrace = this.generate_stacktrace();
761 report_msg(
762 DiagLevel::Note,
763 "the place in the program where the ICE was triggered".to_string(),
764 vec![],
765 vec![],
766 vec![],
767 &stacktrace,
768 Some(this.active_thread()),
769 &this.machine,
770 );
771 }
772}