miri/
diagnostics.rs

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
12/// Details of premature program termination.
13pub enum TerminationInfo {
14    Exit {
15        code: i32,
16        leak_check: bool,
17    },
18    Abort(String),
19    /// Miri was interrupted by a Ctrl+C from the user
20    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    /// In GenMC mode, an execution can get stuck in certain cases. This is not an error.
35    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
117/// Miri specific diagnostics
118pub enum NonHaltingDiagnostic {
119    /// (new_tag, new_perm, (alloc_id, base_offset, orig_tag))
120    ///
121    /// new_perm is `None` for base tags.
122    CreatedPointerTag(NonZero<u64>, Option<String>, Option<(AllocId, AllocRange, ProvenanceExtra)>),
123    /// This `Item` was popped from the borrow stack. The string explains the reason.
124    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, // how many basic blocks have been run so far
131    },
132    Int2Ptr {
133        details: bool,
134    },
135    NativeCallSharedMem {
136        tracing: bool,
137    },
138    WeakMemoryOutdatedLoad {
139        ptr: Pointer,
140    },
141    ExternTypeReborrow,
142}
143
144/// Level of Miri specific diagnostics
145pub enum DiagLevel {
146    Error,
147    Warning,
148    Note,
149}
150
151/// Generate a note/help text without a span.
152macro_rules! note {
153    ($($tt:tt)*) => { (None, format!($($tt)*)) };
154}
155/// Generate a note/help text with a span.
156macro_rules! note_span {
157    ($span:expr, $($tt:tt)*) => { (Some($span), format!($($tt)*)) };
158}
159
160/// Attempts to prune a stacktrace to omit the Rust runtime, and returns a bool indicating if any
161/// frames were pruned. If the stacktrace does not have any local frames, we conclude that it must
162/// be pointing to a problem in the Rust runtime itself, and do not prune it at all.
163pub fn prune_stacktrace<'tcx>(
164    mut stacktrace: Vec<FrameInfo<'tcx>>,
165    machine: &MiriMachine<'tcx>,
166) -> (Vec<FrameInfo<'tcx>>, bool) {
167    match machine.backtrace_style {
168        BacktraceStyle::Off => {
169            // Remove all frames marked with `caller_location` -- that attribute indicates we
170            // usually want to point at the caller, not them.
171            stacktrace.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
172            // Retain one frame so that we can print a span for the error itself
173            stacktrace.truncate(1);
174            (stacktrace, false)
175        }
176        BacktraceStyle::Short => {
177            let original_len = stacktrace.len();
178            // Only prune frames if there is at least one local frame. This check ensures that if
179            // we get a backtrace that never makes it to the user code because it has detected a
180            // bug in the Rust runtime, we don't prune away every frame.
181            let has_local_frame = stacktrace.iter().any(|frame| machine.is_local(frame));
182            if has_local_frame {
183                // Remove all frames marked with `caller_location` -- that attribute indicates we
184                // usually want to point at the caller, not them.
185                stacktrace
186                    .retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
187
188                // This is part of the logic that `std` uses to select the relevant part of a
189                // backtrace. But here, we only look for __rust_begin_short_backtrace, not
190                // __rust_end_short_backtrace because the end symbol comes from a call to the default
191                // panic handler.
192                stacktrace = stacktrace
193                    .into_iter()
194                    .take_while(|frame| {
195                        let def_id = frame.instance.def_id();
196                        let path = machine.tcx.def_path_str(def_id);
197                        !path.contains("__rust_begin_short_backtrace")
198                    })
199                    .collect::<Vec<_>>();
200
201                // After we prune frames from the bottom, there are a few left that are part of the
202                // Rust runtime. So we remove frames until we get to a local symbol, which should be
203                // main or a test.
204                // This len check ensures that we don't somehow remove every frame, as doing so breaks
205                // the primary error message.
206                while stacktrace.len() > 1
207                    && stacktrace.last().is_some_and(|frame| !machine.is_local(frame))
208                {
209                    stacktrace.pop();
210                }
211            }
212            let was_pruned = stacktrace.len() != original_len;
213            (stacktrace, was_pruned)
214        }
215        BacktraceStyle::Full => (stacktrace, false),
216    }
217}
218
219/// Emit a custom diagnostic without going through the miri-engine machinery.
220///
221/// Returns `Some` if this was regular program termination with a given exit code and a `bool` indicating whether a leak check should happen; `None` otherwise.
222pub fn report_error<'tcx>(
223    ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
224    e: InterpErrorInfo<'tcx>,
225) -> Option<(i32, bool)> {
226    use InterpErrorKind::*;
227    use UndefinedBehaviorInfo::*;
228
229    let mut labels = vec![];
230
231    let (title, helps) = if let MachineStop(info) = e.kind() {
232        let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
233        use TerminationInfo::*;
234        let title = match info {
235            &Exit { code, leak_check } => return Some((code, leak_check)),
236            Abort(_) => Some("abnormal termination"),
237            Interrupted => None,
238            UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance | UnsupportedForeignItem(_) =>
239                Some("unsupported operation"),
240            StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
241                Some("Undefined Behavior"),
242            Deadlock => {
243                labels.push(format!("this thread got stuck here"));
244                None
245            }
246            GenmcStuckExecution => {
247                // This case should only happen in GenMC mode. We treat it like a normal program exit.
248                assert!(ecx.machine.data_race.as_genmc_ref().is_some());
249                tracing::info!("GenMC: found stuck execution");
250                return Some((0, true));
251            }
252            MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
253        };
254        #[rustfmt::skip]
255        let helps = match info {
256            UnsupportedInIsolation(_) =>
257                vec![
258                    note!("set `MIRIFLAGS=-Zmiri-disable-isolation` to disable isolation;"),
259                    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"),
260                ],
261            UnsupportedForeignItem(_) => {
262                vec![
263                    note!("this means the program tried to do something Miri does not support; it does not indicate a bug in the program"),
264                ]
265            }
266            StackedBorrowsUb { help, history, .. } => {
267                labels.extend(help.clone());
268                let mut helps = vec![
269                    note!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental"),
270                    note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information"),
271                ];
272                if let Some(TagHistory {created, invalidated, protected}) = history.clone() {
273                    helps.push((Some(created.1), created.0));
274                    if let Some((msg, span)) = invalidated {
275                        helps.push(note_span!(span, "{msg}"));
276                    }
277                    if let Some((protector_msg, protector_span)) = protected {
278                        helps.push(note_span!(protector_span, "{protector_msg}"));
279                    }
280                }
281                helps
282            },
283            TreeBorrowsUb { title: _, details, history } => {
284                let mut helps = vec![
285                    note!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental"),
286                    note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information"),
287                ];
288                for m in details {
289                    helps.push(note!("{m}"));
290                }
291                for event in history.events.clone() {
292                    helps.push(event);
293                }
294                helps
295            }
296            MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
297                vec![
298                    note_span!(*first, "it's first defined here, in crate `{first_crate}`"),
299                    note_span!(*second, "then it's defined here again, in crate `{second_crate}`"),
300                ],
301            SymbolShimClashing { link_name, span } =>
302                vec![note_span!(*span, "the `{link_name}` symbol is defined here")],
303            Int2PtrWithStrictProvenance =>
304                vec![note!("use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead")],
305            DataRace { op1, extra, retag_explain, .. } => {
306                labels.push(format!("(2) just happened here"));
307                let mut helps = vec![note_span!(op1.span, "and (1) occurred earlier here")];
308                if let Some(extra) = extra {
309                    helps.push(note!("{extra}"));
310                    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"));
311                }
312                if *retag_explain {
313                    helps.push(note!("retags occur on all (re)borrows and as well as when references are copied or moved"));
314                    helps.push(note!("retags permit optimizations that insert speculative reads or writes"));
315                    helps.push(note!("therefore from the perspective of data races, a retag has the same implications as a read or write"));
316                }
317                helps.push(note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"));
318                helps.push(note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"));
319                helps
320            }
321                ,
322            _ => vec![],
323        };
324        (title, helps)
325    } else {
326        let title = match e.kind() {
327            UndefinedBehavior(ValidationError(validation_err))
328                if matches!(
329                    validation_err.kind,
330                    ValidationErrorKind::PointerAsInt { .. } | ValidationErrorKind::PartialPointer
331                ) =>
332            {
333                ecx.handle_ice(); // print interpreter backtrace (this is outside the eval `catch_unwind`)
334                bug!(
335                    "This validation error should be impossible in Miri: {}",
336                    format_interp_error(ecx.tcx.dcx(), e)
337                );
338            }
339            UndefinedBehavior(_) => "Undefined Behavior",
340            ResourceExhaustion(_) => "resource exhaustion",
341            Unsupported(
342                // We list only the ones that can actually happen.
343                UnsupportedOpInfo::Unsupported(_)
344                | UnsupportedOpInfo::UnsizedLocal
345                | UnsupportedOpInfo::ExternTypeField,
346            ) => "unsupported operation",
347            InvalidProgram(
348                // We list only the ones that can actually happen.
349                InvalidProgramInfo::AlreadyReported(_) | InvalidProgramInfo::Layout(..),
350            ) => "post-monomorphization error",
351            _ => {
352                ecx.handle_ice(); // print interpreter backtrace (this is outside the eval `catch_unwind`)
353                bug!(
354                    "This error should be impossible in Miri: {}",
355                    format_interp_error(ecx.tcx.dcx(), e)
356                );
357            }
358        };
359        #[rustfmt::skip]
360        let helps = match e.kind() {
361            Unsupported(_) =>
362                vec![
363                    note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
364                ],
365            UndefinedBehavior(AlignmentCheckFailed { .. })
366                if ecx.machine.check_alignment == AlignmentCheck::Symbolic
367            =>
368                vec![
369                    note!("this usually indicates that your program performed an invalid operation and caused Undefined Behavior"),
370                    note!("but due to `-Zmiri-symbolic-alignment-check`, alignment errors can also be false positives"),
371                ],
372            UndefinedBehavior(info) => {
373                let mut helps = vec![
374                    note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"),
375                    note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"),
376                ];
377                match info {
378                    PointerUseAfterFree(alloc_id, _) | PointerOutOfBounds { alloc_id, .. } => {
379                        if let Some(span) = ecx.machine.allocated_span(*alloc_id) {
380                            helps.push(note_span!(span, "{:?} was allocated here:", alloc_id));
381                        }
382                        if let Some(span) = ecx.machine.deallocated_span(*alloc_id) {
383                            helps.push(note_span!(span, "{:?} was deallocated here:", alloc_id));
384                        }
385                    }
386                    AbiMismatchArgument { .. } | AbiMismatchReturn { .. } => {
387                        helps.push(note!("this means these two types are not *guaranteed* to be ABI-compatible across all targets"));
388                        helps.push(note!("if you think this code should be accepted anyway, please report an issue with Miri"));
389                    }
390                    _ => {},
391                }
392                helps
393            }
394            InvalidProgram(
395                InvalidProgramInfo::AlreadyReported(_)
396            ) => {
397                // This got already reported. No point in reporting it again.
398                return None;
399            }
400            _ =>
401                vec![],
402        };
403        (Some(title), helps)
404    };
405
406    let stacktrace = ecx.generate_stacktrace();
407    let (stacktrace, mut any_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
408
409    let mut show_all_threads = false;
410
411    // We want to dump the allocation if this is `InvalidUninitBytes`.
412    // Since `format_interp_error` consumes `e`, we compute the outut early.
413    let mut extra = String::new();
414    match e.kind() {
415        UndefinedBehavior(InvalidUninitBytes(Some((alloc_id, access)))) => {
416            writeln!(
417                extra,
418                "Uninitialized memory occurred at {alloc_id:?}{range:?}, in this allocation:",
419                range = access.bad,
420            )
421            .unwrap();
422            writeln!(extra, "{:?}", ecx.dump_alloc(*alloc_id)).unwrap();
423        }
424        MachineStop(info) => {
425            let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
426            match info {
427                TerminationInfo::Deadlock => {
428                    show_all_threads = true;
429                }
430                _ => {}
431            }
432        }
433        _ => {}
434    }
435
436    let mut primary_msg = String::new();
437    if let Some(title) = title {
438        write!(primary_msg, "{title}: ").unwrap();
439    }
440    write!(primary_msg, "{}", format_interp_error(ecx.tcx.dcx(), e)).unwrap();
441
442    if labels.is_empty() {
443        labels.push(format!("{} occurred here", title.unwrap_or("error")));
444    }
445
446    report_msg(
447        DiagLevel::Error,
448        primary_msg,
449        labels,
450        vec![],
451        helps,
452        &stacktrace,
453        Some(ecx.active_thread()),
454        &ecx.machine,
455    );
456
457    eprint!("{extra}"); // newlines are already in the string
458
459    if show_all_threads {
460        for (thread, stack) in ecx.machine.threads.all_stacks() {
461            if thread != ecx.active_thread() {
462                let stacktrace = Frame::generate_stacktrace_from_stack(stack);
463                let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
464                any_pruned |= was_pruned;
465                report_msg(
466                    DiagLevel::Error,
467                    format!("the evaluated program deadlocked"),
468                    vec![format!("this thread got stuck here")],
469                    vec![],
470                    vec![],
471                    &stacktrace,
472                    Some(thread),
473                    &ecx.machine,
474                )
475            }
476        }
477    }
478
479    // Include a note like `std` does when we omit frames from a backtrace
480    if any_pruned {
481        ecx.tcx.dcx().note(
482            "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
483        );
484    }
485
486    // Debug-dump all locals.
487    for (i, frame) in ecx.active_thread_stack().iter().enumerate() {
488        trace!("-------------------");
489        trace!("Frame {}", i);
490        trace!("    return: {:?}", frame.return_place);
491        for (i, local) in frame.locals.iter().enumerate() {
492            trace!("    local {}: {:?}", i, local);
493        }
494    }
495
496    None
497}
498
499pub fn report_leaks<'tcx>(
500    ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
501    leaks: Vec<(AllocId, MemoryKind, Allocation<Provenance, AllocExtra<'tcx>, MiriAllocBytes>)>,
502) {
503    let mut any_pruned = false;
504    for (id, kind, alloc) in leaks {
505        let mut title = format!(
506            "memory leaked: {id:?} ({}, size: {:?}, align: {:?})",
507            kind,
508            alloc.size().bytes(),
509            alloc.align.bytes()
510        );
511        let Some(backtrace) = alloc.extra.backtrace else {
512            ecx.tcx.dcx().err(title);
513            continue;
514        };
515        title.push_str(", allocated here:");
516        let (backtrace, pruned) = prune_stacktrace(backtrace, &ecx.machine);
517        any_pruned |= pruned;
518        report_msg(
519            DiagLevel::Error,
520            title,
521            vec![],
522            vec![],
523            vec![],
524            &backtrace,
525            None, // we don't know the thread this is from
526            &ecx.machine,
527        );
528    }
529    if any_pruned {
530        ecx.tcx.dcx().note(
531            "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
532        );
533    }
534}
535
536/// Report an error or note (depending on the `error` argument) with the given stacktrace.
537/// Also emits a full stacktrace of the interpreter stack.
538/// We want to present a multi-line span message for some errors. Diagnostics do not support this
539/// directly, so we pass the lines as a `Vec<String>` and display each line after the first with an
540/// additional `span_label` or `note` call.
541pub fn report_msg<'tcx>(
542    diag_level: DiagLevel,
543    title: String,
544    span_msg: Vec<String>,
545    notes: Vec<(Option<SpanData>, String)>,
546    helps: Vec<(Option<SpanData>, String)>,
547    stacktrace: &[FrameInfo<'tcx>],
548    thread: Option<ThreadId>,
549    machine: &MiriMachine<'tcx>,
550) {
551    let span = stacktrace.first().map_or(DUMMY_SP, |fi| fi.span);
552    let sess = machine.tcx.sess;
553    let level = match diag_level {
554        DiagLevel::Error => Level::Error,
555        DiagLevel::Warning => Level::Warning,
556        DiagLevel::Note => Level::Note,
557    };
558    let mut err = Diag::<()>::new(sess.dcx(), level, title);
559    err.span(span);
560
561    // Show main message.
562    if span != DUMMY_SP {
563        for line in span_msg {
564            err.span_label(span, line);
565        }
566    } else {
567        // Make sure we show the message even when it is a dummy span.
568        for line in span_msg {
569            err.note(line);
570        }
571        err.note("(no span available)");
572    }
573
574    // Show note and help messages.
575    let mut extra_span = false;
576    for (span_data, note) in notes {
577        if let Some(span_data) = span_data {
578            err.span_note(span_data.span(), note);
579            extra_span = true;
580        } else {
581            err.note(note);
582        }
583    }
584    for (span_data, help) in helps {
585        if let Some(span_data) = span_data {
586            err.span_help(span_data.span(), help);
587            extra_span = true;
588        } else {
589            err.help(help);
590        }
591    }
592
593    // Add backtrace
594    let mut backtrace_title = String::from("BACKTRACE");
595    if extra_span {
596        write!(backtrace_title, " (of the first span)").unwrap();
597    }
598    if let Some(thread) = thread {
599        let thread_name = machine.threads.get_thread_display_name(thread);
600        if thread_name != "main" {
601            // Only print thread name if it is not `main`.
602            write!(backtrace_title, " on thread `{thread_name}`").unwrap();
603        };
604    }
605    write!(backtrace_title, ":").unwrap();
606    err.note(backtrace_title);
607    for (idx, frame_info) in stacktrace.iter().enumerate() {
608        let is_local = machine.is_local(frame_info);
609        // No span for non-local frames and the first frame (which is the error site).
610        if is_local && idx > 0 {
611            err.subdiagnostic(frame_info.as_note(machine.tcx));
612        } else {
613            let sm = sess.source_map();
614            let span = sm.span_to_embeddable_string(frame_info.span);
615            err.note(format!("{frame_info} at {span}"));
616        }
617    }
618
619    err.emit();
620}
621
622impl<'tcx> MiriMachine<'tcx> {
623    pub fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
624        use NonHaltingDiagnostic::*;
625
626        let stacktrace = Frame::generate_stacktrace_from_stack(self.threads.active_thread_stack());
627        let (stacktrace, _was_pruned) = prune_stacktrace(stacktrace, self);
628
629        let (label, diag_level) = match &e {
630            RejectedIsolatedOp(_) =>
631                ("operation rejected by isolation".to_string(), DiagLevel::Warning),
632            Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning),
633            NativeCallSharedMem { .. } =>
634                ("sharing memory with a native function".to_string(), DiagLevel::Warning),
635            ExternTypeReborrow =>
636                ("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
637            CreatedPointerTag(..)
638            | PoppedPointerTag(..)
639            | CreatedAlloc(..)
640            | AccessedAlloc(..)
641            | FreedAlloc(..)
642            | ProgressReport { .. }
643            | WeakMemoryOutdatedLoad { .. } =>
644                ("tracking was triggered here".to_string(), DiagLevel::Note),
645        };
646
647        let title = match &e {
648            CreatedPointerTag(tag, None, _) => format!("created base tag {tag:?}"),
649            CreatedPointerTag(tag, Some(perm), None) =>
650                format!("created {tag:?} with {perm} derived from unknown tag"),
651            CreatedPointerTag(tag, Some(perm), Some((alloc_id, range, orig_tag))) =>
652                format!(
653                    "created tag {tag:?} with {perm} at {alloc_id:?}{range:?} derived from {orig_tag:?}"
654                ),
655            PoppedPointerTag(item, cause) => format!("popped tracked tag for item {item:?}{cause}"),
656            CreatedAlloc(AllocId(id), size, align, kind) =>
657                format!(
658                    "created {kind} allocation of {size} bytes (alignment {align} bytes) with id {id}",
659                    size = size.bytes(),
660                    align = align.bytes(),
661                ),
662            AccessedAlloc(AllocId(id), access_kind) =>
663                format!("{access_kind} to allocation with id {id}"),
664            FreedAlloc(AllocId(id)) => format!("freed allocation with id {id}"),
665            RejectedIsolatedOp(op) => format!("{op} was made to return an error due to isolation"),
666            ProgressReport { .. } =>
667                format!("progress report: current operation being executed is here"),
668            Int2Ptr { .. } => format!("integer-to-pointer cast"),
669            NativeCallSharedMem { .. } =>
670                format!("sharing memory with a native function called via FFI"),
671            WeakMemoryOutdatedLoad { ptr } =>
672                format!("weak memory emulation: outdated value returned from load at {ptr}"),
673            ExternTypeReborrow =>
674                format!("reborrow of a reference to `extern type` is not properly supported"),
675        };
676
677        let notes = match &e {
678            ProgressReport { block_count } => {
679                vec![note!("so far, {block_count} basic blocks have been executed")]
680            }
681            _ => vec![],
682        };
683
684        let helps = match &e {
685            Int2Ptr { details: true } => {
686                let mut v = vec![
687                    note!(
688                        "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"
689                    ),
690                    note!(
691                        "see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation"
692                    ),
693                    note!(
694                        "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"
695                    ),
696                    note!(
697                        "you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics"
698                    ),
699                ];
700                if self.borrow_tracker.as_ref().is_some_and(|b| {
701                    matches!(
702                        b.borrow().borrow_tracker_method(),
703                        BorrowTrackerMethod::TreeBorrows { .. }
704                    )
705                }) {
706                    v.push(
707                        note!("Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used")
708                    );
709                } else {
710                    v.push(
711                        note!("alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning")
712                    );
713                }
714                v
715            }
716            NativeCallSharedMem { tracing } =>
717                if *tracing {
718                    vec![
719                        note!(
720                            "when memory is shared with a native function call, Miri can only track initialisation and provenance on a best-effort basis"
721                        ),
722                        note!(
723                            "in particular, Miri assumes that the native call initializes all memory it has written to"
724                        ),
725                        note!(
726                            "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory"
727                        ),
728                        note!(
729                            "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"
730                        ),
731                        note!(
732                            "tracing memory accesses in native code is not yet fully implemented, so there can be further imprecisions beyond what is documented here"
733                        ),
734                    ]
735                } else {
736                    vec![
737                        note!(
738                            "when memory is shared with a native function call, Miri stops tracking initialization and provenance for that memory"
739                        ),
740                        note!(
741                            "in particular, Miri assumes that the native call initializes all memory it has access to"
742                        ),
743                        note!(
744                            "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory"
745                        ),
746                        note!(
747                            "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"
748                        ),
749                    ]
750                },
751            ExternTypeReborrow => {
752                assert!(self.borrow_tracker.as_ref().is_some_and(|b| {
753                    matches!(
754                        b.borrow().borrow_tracker_method(),
755                        BorrowTrackerMethod::StackedBorrows
756                    )
757                }));
758                vec![
759                    note!(
760                        "`extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code"
761                    ),
762                    note!(
763                        "try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead"
764                    ),
765                ]
766            }
767            _ => vec![],
768        };
769
770        report_msg(
771            diag_level,
772            title,
773            vec![label],
774            notes,
775            helps,
776            &stacktrace,
777            Some(self.threads.active_thread()),
778            self,
779        );
780    }
781}
782
783impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
784pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
785    fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
786        let this = self.eval_context_ref();
787        this.machine.emit_diagnostic(e);
788    }
789
790    /// We had a panic in Miri itself, try to print something useful.
791    fn handle_ice(&self) {
792        eprintln!();
793        eprintln!(
794            "Miri caused an ICE during evaluation. Here's the interpreter backtrace at the time of the panic:"
795        );
796        let this = self.eval_context_ref();
797        let stacktrace = this.generate_stacktrace();
798        report_msg(
799            DiagLevel::Note,
800            "the place in the program where the ICE was triggered".to_string(),
801            vec![],
802            vec![],
803            vec![],
804            &stacktrace,
805            Some(this.active_thread()),
806            &this.machine,
807        );
808    }
809}