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