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 MultipleSymbolDefinitions {
35 link_name: Symbol,
36 first: SpanData,
37 first_crate: Symbol,
38 second: SpanData,
39 second_crate: Symbol,
40 },
41 SymbolShimClashing {
42 link_name: Symbol,
43 span: SpanData,
44 },
45 DataRace {
46 involves_non_atomic: bool,
47 ptr: interpret::Pointer<AllocId>,
48 op1: RacingOp,
49 op2: RacingOp,
50 extra: Option<&'static str>,
51 retag_explain: bool,
52 },
53 UnsupportedForeignItem(String),
54}
55
56pub struct RacingOp {
57 pub action: String,
58 pub thread_info: String,
59 pub span: SpanData,
60}
61
62impl fmt::Display for TerminationInfo {
63 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
64 use TerminationInfo::*;
65 match self {
66 Exit { code, .. } => write!(f, "the evaluated program completed with exit code {code}"),
67 Abort(msg) => write!(f, "{msg}"),
68 Interrupted => write!(f, "interpretation was interrupted"),
69 UnsupportedInIsolation(msg) => write!(f, "{msg}"),
70 Int2PtrWithStrictProvenance =>
71 write!(
72 f,
73 "integer-to-pointer casts and `ptr::with_exposed_provenance` are not supported with `-Zmiri-strict-provenance`"
74 ),
75 StackedBorrowsUb { msg, .. } => write!(f, "{msg}"),
76 TreeBorrowsUb { title, .. } => write!(f, "{title}"),
77 Deadlock => write!(f, "the evaluated program deadlocked"),
78 MultipleSymbolDefinitions { link_name, .. } =>
79 write!(f, "multiple definitions of symbol `{link_name}`"),
80 SymbolShimClashing { link_name, .. } =>
81 write!(f, "found `{link_name}` symbol definition that clashes with a built-in shim",),
82 DataRace { involves_non_atomic, ptr, op1, op2, .. } =>
83 write!(
84 f,
85 "{} detected between (1) {} on {} and (2) {} on {} at {ptr:?}. (2) just happened here",
86 if *involves_non_atomic { "Data race" } else { "Race condition" },
87 op1.action,
88 op1.thread_info,
89 op2.action,
90 op2.thread_info
91 ),
92 UnsupportedForeignItem(msg) => write!(f, "{msg}"),
93 }
94 }
95}
96
97impl fmt::Debug for TerminationInfo {
98 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
99 write!(f, "{self}")
100 }
101}
102
103impl MachineStopType for TerminationInfo {
104 fn diagnostic_message(&self) -> DiagMessage {
105 self.to_string().into()
106 }
107 fn add_args(
108 self: Box<Self>,
109 _: &mut dyn FnMut(std::borrow::Cow<'static, str>, rustc_errors::DiagArgValue),
110 ) {
111 }
112}
113
114pub enum NonHaltingDiagnostic {
116 CreatedPointerTag(NonZero<u64>, Option<String>, Option<(AllocId, AllocRange, ProvenanceExtra)>),
120 PoppedPointerTag(Item, String),
122 CreatedAlloc(AllocId, Size, Align, MemoryKind),
123 FreedAlloc(AllocId),
124 AccessedAlloc(AllocId, AccessKind),
125 RejectedIsolatedOp(String),
126 ProgressReport {
127 block_count: u64, },
129 Int2Ptr {
130 details: bool,
131 },
132 NativeCallSharedMem,
133 WeakMemoryOutdatedLoad {
134 ptr: Pointer,
135 },
136 ExternTypeReborrow,
137}
138
139pub enum DiagLevel {
141 Error,
142 Warning,
143 Note,
144}
145
146macro_rules! note {
148 ($($tt:tt)*) => { (None, format!($($tt)*)) };
149}
150macro_rules! note_span {
152 ($span:expr, $($tt:tt)*) => { (Some($span), format!($($tt)*)) };
153}
154
155pub fn prune_stacktrace<'tcx>(
159 mut stacktrace: Vec<FrameInfo<'tcx>>,
160 machine: &MiriMachine<'tcx>,
161) -> (Vec<FrameInfo<'tcx>>, bool) {
162 match machine.backtrace_style {
163 BacktraceStyle::Off => {
164 stacktrace.retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
167 stacktrace.truncate(1);
169 (stacktrace, false)
170 }
171 BacktraceStyle::Short => {
172 let original_len = stacktrace.len();
173 let has_local_frame = stacktrace.iter().any(|frame| machine.is_local(frame));
177 if has_local_frame {
178 stacktrace
181 .retain(|frame| !frame.instance.def.requires_caller_location(machine.tcx));
182
183 stacktrace = stacktrace
188 .into_iter()
189 .take_while(|frame| {
190 let def_id = frame.instance.def_id();
191 let path = machine.tcx.def_path_str(def_id);
192 !path.contains("__rust_begin_short_backtrace")
193 })
194 .collect::<Vec<_>>();
195
196 while stacktrace.len() > 1
202 && stacktrace.last().is_some_and(|frame| !machine.is_local(frame))
203 {
204 stacktrace.pop();
205 }
206 }
207 let was_pruned = stacktrace.len() != original_len;
208 (stacktrace, was_pruned)
209 }
210 BacktraceStyle::Full => (stacktrace, false),
211 }
212}
213
214pub fn report_error<'tcx>(
218 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
219 e: InterpErrorInfo<'tcx>,
220) -> Option<(i32, bool)> {
221 use InterpErrorKind::*;
222 use UndefinedBehaviorInfo::*;
223
224 let mut msg = vec![];
225
226 let (title, helps) = if let MachineStop(info) = e.kind() {
227 let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
228 use TerminationInfo::*;
229 let title = match info {
230 &Exit { code, leak_check } => return Some((code, leak_check)),
231 Abort(_) => Some("abnormal termination"),
232 Interrupted => None,
233 UnsupportedInIsolation(_) | Int2PtrWithStrictProvenance | UnsupportedForeignItem(_) =>
234 Some("unsupported operation"),
235 StackedBorrowsUb { .. } | TreeBorrowsUb { .. } | DataRace { .. } =>
236 Some("Undefined Behavior"),
237 Deadlock => Some("deadlock"),
238 MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
239 };
240 #[rustfmt::skip]
241 let helps = match info {
242 UnsupportedInIsolation(_) =>
243 vec![
244 note!("set `MIRIFLAGS=-Zmiri-disable-isolation` to disable isolation;"),
245 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"),
246 ],
247 UnsupportedForeignItem(_) => {
248 vec![
249 note!("if this is a basic API commonly used on this target, please report an issue with Miri"),
250 note!("however, note that Miri does not aim to support every FFI function out there; for instance, we will not support APIs for things such as GUIs, scripting languages, or databases"),
251 ]
252 }
253 StackedBorrowsUb { help, history, .. } => {
254 msg.extend(help.clone());
255 let mut helps = vec![
256 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental"),
257 note!("see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information"),
258 ];
259 if let Some(TagHistory {created, invalidated, protected}) = history.clone() {
260 helps.push((Some(created.1), created.0));
261 if let Some((msg, span)) = invalidated {
262 helps.push(note_span!(span, "{msg}"));
263 }
264 if let Some((protector_msg, protector_span)) = protected {
265 helps.push(note_span!(protector_span, "{protector_msg}"));
266 }
267 }
268 helps
269 },
270 TreeBorrowsUb { title: _, details, history } => {
271 let mut helps = vec![
272 note!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")
273 ];
274 for m in details {
275 helps.push(note!("{m}"));
276 }
277 for event in history.events.clone() {
278 helps.push(event);
279 }
280 helps
281 }
282 MultipleSymbolDefinitions { first, first_crate, second, second_crate, .. } =>
283 vec![
284 note_span!(*first, "it's first defined here, in crate `{first_crate}`"),
285 note_span!(*second, "then it's defined here again, in crate `{second_crate}`"),
286 ],
287 SymbolShimClashing { link_name, span } =>
288 vec![note_span!(*span, "the `{link_name}` symbol is defined here")],
289 Int2PtrWithStrictProvenance =>
290 vec![note!("use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead")],
291 DataRace { op1, extra, retag_explain, .. } => {
292 let mut helps = vec![note_span!(op1.span, "and (1) occurred earlier here")];
293 if let Some(extra) = extra {
294 helps.push(note!("{extra}"));
295 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"));
296 }
297 if *retag_explain {
298 helps.push(note!("retags occur on all (re)borrows and as well as when references are copied or moved"));
299 helps.push(note!("retags permit optimizations that insert speculative reads or writes"));
300 helps.push(note!("therefore from the perspective of data races, a retag has the same implications as a read or write"));
301 }
302 helps.push(note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"));
303 helps.push(note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"));
304 helps
305 }
306 ,
307 _ => vec![],
308 };
309 (title, helps)
310 } else {
311 let title = match e.kind() {
312 UndefinedBehavior(ValidationError(validation_err))
313 if matches!(
314 validation_err.kind,
315 ValidationErrorKind::PointerAsInt { .. } | ValidationErrorKind::PartialPointer
316 ) =>
317 {
318 ecx.handle_ice(); bug!(
320 "This validation error should be impossible in Miri: {}",
321 format_interp_error(ecx.tcx.dcx(), e)
322 );
323 }
324 UndefinedBehavior(_) => "Undefined Behavior",
325 ResourceExhaustion(_) => "resource exhaustion",
326 Unsupported(
327 UnsupportedOpInfo::Unsupported(_)
329 | UnsupportedOpInfo::UnsizedLocal
330 | UnsupportedOpInfo::ExternTypeField,
331 ) => "unsupported operation",
332 InvalidProgram(
333 InvalidProgramInfo::AlreadyReported(_) | InvalidProgramInfo::Layout(..),
335 ) => "post-monomorphization error",
336 _ => {
337 ecx.handle_ice(); bug!(
339 "This error should be impossible in Miri: {}",
340 format_interp_error(ecx.tcx.dcx(), e)
341 );
342 }
343 };
344 #[rustfmt::skip]
345 let helps = match e.kind() {
346 Unsupported(_) =>
347 vec![
348 note!("this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support"),
349 ],
350 UndefinedBehavior(AlignmentCheckFailed { .. })
351 if ecx.machine.check_alignment == AlignmentCheck::Symbolic
352 =>
353 vec![
354 note!("this usually indicates that your program performed an invalid operation and caused Undefined Behavior"),
355 note!("but due to `-Zmiri-symbolic-alignment-check`, alignment errors can also be false positives"),
356 ],
357 UndefinedBehavior(info) => {
358 let mut helps = vec![
359 note!("this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior"),
360 note!("see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information"),
361 ];
362 match info {
363 PointerUseAfterFree(alloc_id, _) | PointerOutOfBounds { alloc_id, .. } => {
364 if let Some(span) = ecx.machine.allocated_span(*alloc_id) {
365 helps.push(note_span!(span, "{:?} was allocated here:", alloc_id));
366 }
367 if let Some(span) = ecx.machine.deallocated_span(*alloc_id) {
368 helps.push(note_span!(span, "{:?} was deallocated here:", alloc_id));
369 }
370 }
371 AbiMismatchArgument { .. } | AbiMismatchReturn { .. } => {
372 helps.push(note!("this means these two types are not *guaranteed* to be ABI-compatible across all targets"));
373 helps.push(note!("if you think this code should be accepted anyway, please report an issue with Miri"));
374 }
375 _ => {},
376 }
377 helps
378 }
379 InvalidProgram(
380 InvalidProgramInfo::AlreadyReported(_)
381 ) => {
382 return None;
384 }
385 _ =>
386 vec![],
387 };
388 (Some(title), helps)
389 };
390
391 let stacktrace = ecx.generate_stacktrace();
392 let (stacktrace, mut any_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
393
394 let mut show_all_threads = false;
395
396 let mut extra = String::new();
399 match e.kind() {
400 UndefinedBehavior(InvalidUninitBytes(Some((alloc_id, access)))) => {
401 writeln!(
402 extra,
403 "Uninitialized memory occurred at {alloc_id:?}{range:?}, in this allocation:",
404 range = access.bad,
405 )
406 .unwrap();
407 writeln!(extra, "{:?}", ecx.dump_alloc(*alloc_id)).unwrap();
408 }
409 MachineStop(info) => {
410 let info = info.downcast_ref::<TerminationInfo>().expect("invalid MachineStop payload");
411 match info {
412 TerminationInfo::Deadlock => {
413 show_all_threads = true;
414 }
415 _ => {}
416 }
417 }
418 _ => {}
419 }
420
421 msg.insert(0, format_interp_error(ecx.tcx.dcx(), e));
422
423 report_msg(
424 DiagLevel::Error,
425 if let Some(title) = title { format!("{title}: {}", msg[0]) } else { msg[0].clone() },
426 msg,
427 vec![],
428 helps,
429 &stacktrace,
430 Some(ecx.active_thread()),
431 &ecx.machine,
432 );
433
434 eprint!("{extra}"); if show_all_threads {
437 for (thread, stack) in ecx.machine.threads.all_stacks() {
438 if thread != ecx.active_thread() {
439 let stacktrace = Frame::generate_stacktrace_from_stack(stack);
440 let (stacktrace, was_pruned) = prune_stacktrace(stacktrace, &ecx.machine);
441 any_pruned |= was_pruned;
442 report_msg(
443 DiagLevel::Error,
444 format!("deadlock: the evaluated program deadlocked"),
445 vec![format!("the evaluated program deadlocked")],
446 vec![],
447 vec![],
448 &stacktrace,
449 Some(thread),
450 &ecx.machine,
451 )
452 }
453 }
454 }
455
456 if any_pruned {
458 ecx.tcx.dcx().note(
459 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
460 );
461 }
462
463 for (i, frame) in ecx.active_thread_stack().iter().enumerate() {
465 trace!("-------------------");
466 trace!("Frame {}", i);
467 trace!(" return: {:?}", frame.return_place);
468 for (i, local) in frame.locals.iter().enumerate() {
469 trace!(" local {}: {:?}", i, local);
470 }
471 }
472
473 None
474}
475
476pub fn report_leaks<'tcx>(
477 ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
478 leaks: Vec<(AllocId, MemoryKind, Allocation<Provenance, AllocExtra<'tcx>, MiriAllocBytes>)>,
479) {
480 let mut any_pruned = false;
481 for (id, kind, alloc) in leaks {
482 let mut title = format!(
483 "memory leaked: {id:?} ({}, size: {:?}, align: {:?})",
484 kind,
485 alloc.size().bytes(),
486 alloc.align.bytes()
487 );
488 let Some(backtrace) = alloc.extra.backtrace else {
489 ecx.tcx.dcx().err(title);
490 continue;
491 };
492 title.push_str(", allocated here:");
493 let (backtrace, pruned) = prune_stacktrace(backtrace, &ecx.machine);
494 any_pruned |= pruned;
495 report_msg(
496 DiagLevel::Error,
497 title,
498 vec![],
499 vec![],
500 vec![],
501 &backtrace,
502 None, &ecx.machine,
504 );
505 }
506 if any_pruned {
507 ecx.tcx.dcx().note(
508 "some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace",
509 );
510 }
511}
512
513pub fn report_msg<'tcx>(
519 diag_level: DiagLevel,
520 title: String,
521 span_msg: Vec<String>,
522 notes: Vec<(Option<SpanData>, String)>,
523 helps: Vec<(Option<SpanData>, String)>,
524 stacktrace: &[FrameInfo<'tcx>],
525 thread: Option<ThreadId>,
526 machine: &MiriMachine<'tcx>,
527) {
528 let span = stacktrace.first().map_or(DUMMY_SP, |fi| fi.span);
529 let sess = machine.tcx.sess;
530 let level = match diag_level {
531 DiagLevel::Error => Level::Error,
532 DiagLevel::Warning => Level::Warning,
533 DiagLevel::Note => Level::Note,
534 };
535 let mut err = Diag::<()>::new(sess.dcx(), level, title);
536 err.span(span);
537
538 if span != DUMMY_SP {
540 for line in span_msg {
541 err.span_label(span, line);
542 }
543 } else {
544 for line in span_msg {
546 err.note(line);
547 }
548 err.note("(no span available)");
549 }
550
551 let mut extra_span = false;
553 for (span_data, note) in notes {
554 if let Some(span_data) = span_data {
555 err.span_note(span_data.span(), note);
556 extra_span = true;
557 } else {
558 err.note(note);
559 }
560 }
561 for (span_data, help) in helps {
562 if let Some(span_data) = span_data {
563 err.span_help(span_data.span(), help);
564 extra_span = true;
565 } else {
566 err.help(help);
567 }
568 }
569
570 let mut backtrace_title = String::from("BACKTRACE");
572 if extra_span {
573 write!(backtrace_title, " (of the first span)").unwrap();
574 }
575 if let Some(thread) = thread {
576 let thread_name = machine.threads.get_thread_display_name(thread);
577 if thread_name != "main" {
578 write!(backtrace_title, " on thread `{thread_name}`").unwrap();
580 };
581 }
582 write!(backtrace_title, ":").unwrap();
583 err.note(backtrace_title);
584 for (idx, frame_info) in stacktrace.iter().enumerate() {
585 let is_local = machine.is_local(frame_info);
586 if is_local && idx > 0 {
588 err.subdiagnostic(frame_info.as_note(machine.tcx));
589 } else {
590 let sm = sess.source_map();
591 let span = sm.span_to_embeddable_string(frame_info.span);
592 err.note(format!("{frame_info} at {span}"));
593 }
594 }
595
596 err.emit();
597}
598
599impl<'tcx> MiriMachine<'tcx> {
600 pub fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
601 use NonHaltingDiagnostic::*;
602
603 let stacktrace = Frame::generate_stacktrace_from_stack(self.threads.active_thread_stack());
604 let (stacktrace, _was_pruned) = prune_stacktrace(stacktrace, self);
605
606 let (title, diag_level) = match &e {
607 RejectedIsolatedOp(_) =>
608 ("operation rejected by isolation".to_string(), DiagLevel::Warning),
609 Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning),
610 NativeCallSharedMem =>
611 ("sharing memory with a native function".to_string(), DiagLevel::Warning),
612 ExternTypeReborrow =>
613 ("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
614 CreatedPointerTag(..)
615 | PoppedPointerTag(..)
616 | CreatedAlloc(..)
617 | AccessedAlloc(..)
618 | FreedAlloc(..)
619 | ProgressReport { .. }
620 | WeakMemoryOutdatedLoad { .. } =>
621 ("tracking was triggered".to_string(), DiagLevel::Note),
622 };
623
624 let msg = match &e {
625 CreatedPointerTag(tag, None, _) => format!("created base tag {tag:?}"),
626 CreatedPointerTag(tag, Some(perm), None) =>
627 format!("created {tag:?} with {perm} derived from unknown tag"),
628 CreatedPointerTag(tag, Some(perm), Some((alloc_id, range, orig_tag))) =>
629 format!(
630 "created tag {tag:?} with {perm} at {alloc_id:?}{range:?} derived from {orig_tag:?}"
631 ),
632 PoppedPointerTag(item, cause) => format!("popped tracked tag for item {item:?}{cause}"),
633 CreatedAlloc(AllocId(id), size, align, kind) =>
634 format!(
635 "created {kind} allocation of {size} bytes (alignment {align} bytes) with id {id}",
636 size = size.bytes(),
637 align = align.bytes(),
638 ),
639 AccessedAlloc(AllocId(id), access_kind) =>
640 format!("{access_kind} to allocation with id {id}"),
641 FreedAlloc(AllocId(id)) => format!("freed allocation with id {id}"),
642 RejectedIsolatedOp(ref op) =>
643 format!("{op} was made to return an error due to isolation"),
644 ProgressReport { .. } =>
645 format!("progress report: current operation being executed is here"),
646 Int2Ptr { .. } => format!("integer-to-pointer cast"),
647 NativeCallSharedMem => format!("sharing memory with a native function called via FFI"),
648 WeakMemoryOutdatedLoad { ptr } =>
649 format!("weak memory emulation: outdated value returned from load at {ptr}"),
650 ExternTypeReborrow =>
651 format!("reborrow of a reference to `extern type` is not properly supported"),
652 };
653
654 let notes = match &e {
655 ProgressReport { block_count } => {
656 vec![note!("so far, {block_count} basic blocks have been executed")]
657 }
658 _ => vec![],
659 };
660
661 let helps = match &e {
662 Int2Ptr { details: true } => {
663 let mut v = vec![
664 note!(
665 "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"
666 ),
667 note!(
668 "see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation"
669 ),
670 note!(
671 "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"
672 ),
673 note!(
674 "you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics"
675 ),
676 ];
677 if self.borrow_tracker.as_ref().is_some_and(|b| {
678 matches!(b.borrow().borrow_tracker_method(), BorrowTrackerMethod::TreeBorrows)
679 }) {
680 v.push(
681 note!("Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used")
682 );
683 } else {
684 v.push(
685 note!("alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning")
686 );
687 }
688 v
689 }
690 NativeCallSharedMem => {
691 vec![
692 note!(
693 "when memory is shared with a native function call, Miri stops tracking initialization and provenance for that memory"
694 ),
695 note!(
696 "in particular, Miri assumes that the native call initializes all memory it has access to"
697 ),
698 note!(
699 "Miri also assumes that any part of this memory may be a pointer that is permitted to point to arbitrary exposed memory"
700 ),
701 note!(
702 "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"
703 ),
704 ]
705 }
706 ExternTypeReborrow => {
707 assert!(self.borrow_tracker.as_ref().is_some_and(|b| {
708 matches!(
709 b.borrow().borrow_tracker_method(),
710 BorrowTrackerMethod::StackedBorrows
711 )
712 }));
713 vec![
714 note!(
715 "`extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code"
716 ),
717 note!(
718 "try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead"
719 ),
720 ]
721 }
722 _ => vec![],
723 };
724
725 report_msg(
726 diag_level,
727 title,
728 vec![msg],
729 notes,
730 helps,
731 &stacktrace,
732 Some(self.threads.active_thread()),
733 self,
734 );
735 }
736}
737
738impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
739pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
740 fn emit_diagnostic(&self, e: NonHaltingDiagnostic) {
741 let this = self.eval_context_ref();
742 this.machine.emit_diagnostic(e);
743 }
744
745 fn handle_ice(&self) {
747 eprintln!();
748 eprintln!(
749 "Miri caused an ICE during evaluation. Here's the interpreter backtrace at the time of the panic:"
750 );
751 let this = self.eval_context_ref();
752 let stacktrace = this.generate_stacktrace();
753 report_msg(
754 DiagLevel::Note,
755 "the place in the program where the ICE was triggered".to_string(),
756 vec![],
757 vec![],
758 vec![],
759 &stacktrace,
760 Some(this.active_thread()),
761 &this.machine,
762 );
763 }
764}