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