Skip to content

Commit

Permalink
Make MIRAI diagnostic message easier to identify (#24)
Browse files Browse the repository at this point in the history 
* Make MIRAI diagnostic message easier to identify

* clean up diagnostic message
  • Loading branch information
@seanrion
seanrion authored Dec 16, 2024
1 parent 0d2b4d0 commit 0baad63
Show file tree
Hide file tree
Showing 6 changed files with 61 additions and 69 deletions.
16 changes: 8 additions & 8 deletions Cargo.lock
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Binary file modified binaries/summary_store.tar
View file
Binary file not shown.
46 changes: 22 additions & 24 deletions checker/src/block_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -374,7 +374,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
format!(
"unknown tag type for constant-time verification: {tag_name}",
"[MIRAI] unknown tag type for constant-time verification: {tag_name}",
),
);
self.bv.emit_diagnostic(warning);
Expand Down Expand Up @@ -973,7 +973,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
// Give a diagnostic about this call, and make it the programmer's problem.
let warning = self.bv.cv.session.dcx().struct_span_warn(
self.bv.current_span,
"the called function did not resolve to an implementation with a MIR body",
"[MIRAI] the called function did not resolve to an implementation with a MIR body",
);
self.bv.emit_diagnostic(warning);
}
Expand Down Expand Up @@ -1164,7 +1164,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.cv
.session
.dcx()
.struct_span_warn(span, diagnostic.as_ref().to_string());
.struct_span_warn(span, "[MIRAI] ".to_string() + diagnostic.as_ref());
for pc_span in precondition.spans.iter() {
let snippet = self.bv.tcx.sess.source_map().span_to_snippet(*pc_span);
if snippet.is_ok() {
Expand Down Expand Up @@ -1203,7 +1203,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
let span = self.bv.current_span;
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
"multiple post conditions must be on the same execution path",
"[MIRAI] multiple post conditions must be on the same execution path",
);
self.bv.emit_diagnostic(warning);
}
Expand Down Expand Up @@ -1239,7 +1239,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
if !entry_cond_as_bool.unwrap_or(true) {
let span = self.bv.current_span.source_callsite();
let message =
"this is unreachable, mark it as such by using the verify_unreachable! macro";
"[MIRAI] this is unreachable, mark it as such by using the verify_unreachable! macro";
let warning = self.bv.cv.session.dcx().struct_span_warn(span, message);
self.bv.emit_diagnostic(warning);
return None;
Expand All @@ -1253,9 +1253,9 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
if function_name == KnownNames::MiraiPostcondition {
let span = self.bv.current_span.source_callsite();
let msg = if cond_as_bool.is_some() {
"provably false postcondition"
"[MIRAI] provably false postcondition"
} else {
"possible unsatisfied postcondition"
"[MIRAI] possible unsatisfied postcondition"
};
let warning = self.bv.cv.session.dcx().struct_span_warn(span, msg);
self.bv.emit_diagnostic(warning);
Expand All @@ -1278,7 +1278,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.cv
.session
.dcx()
.struct_span_warn(span, "provably false verification condition");
.struct_span_warn(span, "[MIRAI] provably false verification condition");
self.bv.emit_diagnostic(warning);
if entry_cond_as_bool.is_none()
&& self.bv.preconditions.len() < k_limits::MAX_INFERRED_PRECONDITIONS
Expand Down Expand Up @@ -1329,7 +1329,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.cv
.session
.dcx()
.struct_span_warn(span, warning.clone());
.struct_span_warn(span, "[MIRAI] ".to_string() + warning.clone().as_ref());
self.bv.emit_diagnostic(warning);
}
}
Expand Down Expand Up @@ -1413,7 +1413,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
format!(
"the {} {} have a {} tag",
"[MIRAI] the {} {} have a {} tag",
value_name,
if checking_presence { "may not" } else { "may" },
tag_name
Expand All @@ -1427,7 +1427,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
format!(
"the {value_name} may have a {tag_name} tag, \
"[MIRAI] the {value_name} may have a {tag_name} tag, \
and the tag check cannot be promoted as a precondition, \
because it contains local variables",
),
Expand All @@ -1440,11 +1440,10 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
// The existence of the tag on the value is different from the expectation.
// In this case, report an error.
let span = self.bv.current_span.source_callsite();
let warning =
self.bv.cv.session.dcx().struct_span_warn(
span,
format!("the {value_name} has a {tag_name} tag"),
);
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
format!("[MIRAI] the {value_name} has a {tag_name} tag"),
);
self.bv.emit_diagnostic(warning);
}

Expand Down Expand Up @@ -1555,7 +1554,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.cv
.session
.dcx()
.struct_span_warn(span, error.to_string());
.struct_span_warn(span, "[MIRAI] ".to_string() + error);
self.bv.emit_diagnostic(warning);
// No need to push a precondition, the caller can never satisfy it.
return;
Expand Down Expand Up @@ -1587,7 +1586,8 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
&& self.bv.cv.options.diag_level >= DiagLevel::Library)
{
// Can't make this the caller's problem.
let warning = format!("possible {}", get_assert_msg_description(msg));
let warning =
format!("[MIRAI] possible {}", get_assert_msg_description(msg));
let span = self.bv.current_span;
let warning = self.bv.cv.session.dcx().struct_span_warn(span, warning);
self.bv.emit_diagnostic(warning);
Expand Down Expand Up @@ -1704,12 +1704,10 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
#[logfn_inputs(TRACE)]
fn visit_inline_asm(&mut self, targets: &[mir::BasicBlock]) {
let span = self.bv.current_span;
let warning = self
.bv
.cv
.session
.dcx()
.struct_span_warn(span, "Inline assembly code cannot be analyzed by MIRAI.");
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
"[MIRAI] Inline assembly code cannot be analyzed by MIRAI.",
);
self.bv.emit_diagnostic(warning);
// Don't stop the analysis if we are building a call graph.
self.bv.analysis_is_incomplete = self.bv.cv.options.call_graph_config.is_none();
Expand Down
19 changes: 9 additions & 10 deletions checker/src/body_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -305,11 +305,10 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
fn report_timeout(&mut self, elapsed_time_in_seconds: u64) {
// This body is beyond MIRAI for now
if self.cv.options.diag_level != DiagLevel::Default {
let warning = self
.cv
.session
.dcx()
.struct_span_warn(self.current_span, "The analysis of this function timed out");
let warning = self.cv.session.dcx().struct_span_warn(
self.current_span,
"[MIRAI] The analysis of this function timed out",
);
self.emit_diagnostic(warning);
}
warn!(
Expand Down Expand Up @@ -1128,7 +1127,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
//todo: eventually give a warning if in_range_as_bool is unknown. For now, that is too noisy.
if entry_cond_as_bool.unwrap_or(true) && !in_range_as_bool.unwrap_or(true) {
let span = self.current_span;
let message = "effective offset is outside allocated range";
let message = "[MIRAI] effective offset is outside allocated range";
let warning = self.cv.session.dcx().struct_span_warn(span, message);
self.emit_diagnostic(warning);
}
Expand Down Expand Up @@ -1564,7 +1563,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
if *old_source == LayoutSource::DeAlloc {
let warning = self.cv.session.dcx().struct_span_warn(
self.current_span,
"the pointer points to memory that has already been deallocated",
"[MIRAI] the pointer points to memory that has already been deallocated",
);
self.emit_diagnostic(warning);
}
Expand All @@ -1576,7 +1575,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
if entry_cond_as_bool.unwrap_or(true) && !layouts_match_as_bool.unwrap_or(false) {
// The condition may be reachable and it may be false
let message = format!(
"{}{} the pointer with layout information inconsistent with the allocation",
"[MIRAI] {}{} the pointer with layout information inconsistent with the allocation",
if entry_cond_as_bool.is_none() || layouts_match_as_bool.is_none() {
"possibly "
} else {
Expand Down Expand Up @@ -2013,7 +2012,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
if source_field_index >= source_len {
let warning = self.cv.session.dcx().struct_span_warn(
self.current_span,
"The union is not fully initialized by this assignment",
"[MIRAI] The union is not fully initialized by this assignment",
);
self.emit_diagnostic(warning);
break;
Expand Down Expand Up @@ -2113,7 +2112,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
if source_field_index >= source_len {
let warning = self.cv.session.dcx().struct_span_warn(
self.current_span,
"The union is not fully initialized by this assignment",
"[MIRAI] The union is not fully initialized by this assignment",
);
self.emit_diagnostic(warning);
break;
Expand Down
Loading

0 comments on commit 0baad63

Please sign in to comment.