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!("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(); // print interpreter backtrace (this is outside the eval `catch_unwind`)
328                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                // We list only the ones that can actually happen.
337                UnsupportedOpInfo::Unsupported(_)
338                | UnsupportedOpInfo::UnsizedLocal
339                | UnsupportedOpInfo::ExternTypeField,
340            ) => "unsupported operation",
341            InvalidProgram(
342                // We list only the ones that can actually happen.
343                InvalidProgramInfo::AlreadyReported(_) | InvalidProgramInfo::Layout(..),
344            ) => "post-monomorphization error",
345            _ => {
346                ecx.handle_ice(); // print interpreter backtrace (this is outside the eval `catch_unwind`)
347                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                // This got already reported. No point in reporting it again.
392                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    // We want to dump the allocation if this is `InvalidUninitBytes`.
406    // Since `format_interp_error` consumes `e`, we compute the outut early.
407    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}"); // newlines are already in the string
444
445    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    // Include a note like `std` does when we omit frames from a backtrace
466    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    // Debug-dump all locals.
473    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, // we don't know the thread this is from
512            &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
522/// Report an error or note (depending on the `error` argument) with the given stacktrace.
523/// Also emits a full stacktrace of the interpreter stack.
524/// We want to present a multi-line span message for some errors. Diagnostics do not support this
525/// directly, so we pass the lines as a `Vec<String>` and display each line after the first with an
526/// additional `span_label` or `note` call.
527pub 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    // Show main message.
548    if span != DUMMY_SP {
549        for line in span_msg {
550            err.span_label(span, line);
551        }
552    } else {
553        // Make sure we show the message even when it is a dummy span.
554        for line in span_msg {
555            err.note(line);
556        }
557        err.note("(no span available)");
558    }
559
560    // Show note and help messages.
561    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    // Add backtrace
580    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            // Only print thread name if it is not `main`.
588            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        // No span for non-local frames and the first frame (which is the error site).
596        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    /// We had a panic in Miri itself, try to print something useful.
754    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}