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