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