mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix progress report being deduplicated

Browse Source
This commit is contained in:
Ralf Jung 2022-08-31 14:44:36 +02:00
parent feeeba2925
commit 4cb26afc0c
2 changed files with 55 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

70
src/diagnostics.rs
View File

@ -70,7 +70,9 @@ pub enum NonHaltingDiagnostic {
CreatedAlloc(AllocId, Size, Align, MemoryKind<MiriMemoryKind>),
FreedAlloc(AllocId),
RejectedIsolatedOp(String),
ProgressReport,
ProgressReport {
block_count: u64, // how many basic blocks have been run so far
},
Int2Ptr {
details: bool,
},
@ -261,6 +263,7 @@ pub fn report_error<'tcx, 'mir>(
DiagLevel::Error,
&if let Some(title) = title { format!("{}: {}", title, msg[0]) } else { msg[0].clone() },
msg,
vec![],
helps,
&stacktrace,
);
@ -307,6 +310,7 @@ fn report_msg<'mir, 'tcx>(
diag_level: DiagLevel,
title: &str,
span_msg: Vec<String>,
notes: Vec<(Option<SpanData>, String)>,
helps: Vec<(Option<SpanData>, String)>,
stacktrace: &[FrameInfo<'tcx>],
) {
@ -331,15 +335,22 @@ fn report_msg<'mir, 'tcx>(
err.note("(no span available)");
}
// Show help messages.
if !helps.is_empty() {
for (span_data, help) in helps {
if let Some(span_data) = span_data {
err.span_help(span_data.span(), &help);
} else {
err.help(&help);
}
// Show note and help messages.
for (span_data, note) in &notes {
if let Some(span_data) = span_data {
err.span_note(span_data.span(), note);
} else {
err.note(note);
}
}
for (span_data, help) in &helps {
if let Some(span_data) = span_data {
err.span_help(span_data.span(), help);
} else {
err.help(help);
}
}
if notes.len() + helps.len() > 0 {
// Add visual separator before backtrace.
err.note("backtrace:");
}
@ -436,6 +447,21 @@ fn process_diagnostics(&self, info: TopFrameInfo<'tcx>) {
// Show diagnostics.
for e in diagnostics.drain(..) {
use NonHaltingDiagnostic::*;
let (title, diag_level) = match e {
RejectedIsolatedOp(_) =>
("operation rejected by isolation", DiagLevel::Warning),
Int2Ptr { .. } => ("integer-to-pointer cast", DiagLevel::Warning),
CreatedPointerTag(..)
| PoppedPointerTag(..)
| CreatedCallId(..)
| CreatedAlloc(..)
| FreedAlloc(..)
| ProgressReport { .. }
| WeakMemoryOutdatedLoad =>
("tracking was triggered", DiagLevel::Note),
};
let msg = match e {
CreatedPointerTag(tag, None) =>
format!("created tag {tag:?}"),
@ -465,7 +491,7 @@ fn process_diagnostics(&self, info: TopFrameInfo<'tcx>) {
format!("freed allocation with id {id}"),
RejectedIsolatedOp(ref op) =>
format!("{op} was made to return an error due to isolation"),
ProgressReport =>
ProgressReport { .. } =>
format!("progress report: current operation being executed is here"),
Int2Ptr { .. } =>
format!("integer-to-pointer cast"),
@ -473,18 +499,15 @@ fn process_diagnostics(&self, info: TopFrameInfo<'tcx>) {
format!("weak memory emulation: outdated value returned from load"),
};
let (title, diag_level) = match e {
RejectedIsolatedOp(_) =>
("operation rejected by isolation", DiagLevel::Warning),
Int2Ptr { .. } => ("integer-to-pointer cast", DiagLevel::Warning),
CreatedPointerTag(..)
| PoppedPointerTag(..)
| CreatedCallId(..)
| CreatedAlloc(..)
| FreedAlloc(..)
| ProgressReport
| WeakMemoryOutdatedLoad =>
("tracking was triggered", DiagLevel::Note),
let notes = match e {
ProgressReport { block_count } => {
// It is important that each progress report is slightly different, since
// identical diagnostics are being deduplicated.
vec![
(None, format!("so far, {block_count} basic blocks have been executed")),
]
}
_ => vec![],
};
let helps = match e {
@ -500,7 +523,7 @@ fn process_diagnostics(&self, info: TopFrameInfo<'tcx>) {
_ => vec![],
};
report_msg(this, diag_level, title, vec![msg], helps, &stacktrace);
report_msg(this, diag_level, title, vec![msg], notes, helps, &stacktrace);
}
});
}
@ -519,6 +542,7 @@ fn handle_ice(&self) {
"the place in the program where the ICE was triggered",
vec![],
vec![],
vec![],
&stacktrace,
);
}

16
src/machine.rs
View File

@ -374,8 +374,8 @@ pub struct Evaluator<'mir, 'tcx> {
/// If `Some`, we will report the current stack every N basic blocks.
pub(crate) report_progress: Option<u32>,
/// The number of blocks that passed since the last progress report.
pub(crate) since_progress_report: u32,
// The total number of blocks that have been executed.
pub(crate) basic_block_count: u64,
/// Handle of the optional shared object file for external functions.
pub external_so_lib: Option<(libloading::Library, std::path::PathBuf)>,
@ -433,7 +433,7 @@ pub(crate) fn new(config: &MiriConfig, layout_cx: LayoutCx<'tcx, TyCtxt<'tcx>>)
weak_memory: config.weak_memory_emulation,
preemption_rate: config.preemption_rate,
report_progress: config.report_progress,
since_progress_report: 0,
basic_block_count: 0,
external_so_lib: config.external_so_file.as_ref().map(|lib_file_path| {
// Check if host target == the session target.
if env!("TARGET") != target_triple {
@ -992,14 +992,14 @@ fn stack_mut<'a>(
}
fn before_terminator(ecx: &mut InterpCx<'mir, 'tcx, Self>) -> InterpResult<'tcx> {
ecx.machine.basic_block_count += 1u64; // a u64 that is only incremented by 1 will "never" overflow
// Possibly report our progress.
if let Some(report_progress) = ecx.machine.report_progress {
if ecx.machine.since_progress_report >= report_progress {
register_diagnostic(NonHaltingDiagnostic::ProgressReport);
ecx.machine.since_progress_report = 0;
if ecx.machine.basic_block_count % u64::from(report_progress) == 0 {
register_diagnostic(NonHaltingDiagnostic::ProgressReport {
block_count: ecx.machine.basic_block_count,
});
}
// Cannot overflow, since it is strictly less than `report_progress`.
ecx.machine.since_progress_report += 1;
}
// These are our preemption points.
ecx.maybe_preempt_active_thread();