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