Skip to content

Commit

Permalink
Make MIRAI diagnostic message easier to identify
Browse files Browse the repository at this point in the history
  • Loading branch information
@seanrion
seanrion committed Dec 14, 2024
1 parent 0d2b4d0 commit 3d39f0e
Show file tree
Hide file tree
Showing 4 changed files with 41 additions and 41 deletions.
36 changes: 18 additions & 18 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 @@ -954,7 +954,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
{
let precondition = Precondition {
condition: promotable_entry_condition.logical_not(),
message: Rc::from("incomplete analysis of call because of a nested call to a function without a MIR body"),
message: Rc::from("[MIRAI] incomplete analysis of call because of a nested call to a function without a MIR body"),
provenance: None,
spans: vec![self.bv.current_span.source_callsite()],
};
Expand All @@ -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 All @@ -1287,7 +1287,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
// promote the path as a precondition. I.e. the program is only correct,
// albeit badly written, if we never get here.
let condition = promotable_entry_cond.logical_not();
let message = Rc::from(format!("possible {message}"));
let message = Rc::from(format!("[MIRAI] possible {message}"));
let precondition = Precondition {
condition,
message,
Expand All @@ -1300,7 +1300,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
return None;
}

let warning = format!("possible {message}");
let warning = format!("[MIRAI] possible {message}");

// We might get here, or not, and the condition might be false, or not.
// Give a warning if we don't know all of the callers, or if we run into a k-limit
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 @@ -1443,7 +1443,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} has a {tag_name} tag"),
format!("[MIRAI] the {value_name} has a {tag_name} tag"),
);
self.bv.emit_diagnostic(warning);
}
Expand All @@ -1465,7 +1465,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
let precondition = Precondition {
condition,
message: Rc::from(format!(
"the {} {} have a {} tag",
"[MIRAI] the {} {} have a {} tag",
value_name,
if checking_presence { "may not" } else { "may" },
tag_name
Expand Down Expand Up @@ -1555,7 +1555,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 +1587,7 @@ 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 @@ -1709,7 +1709,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.cv
.session
.dcx()
.struct_span_warn(span, "Inline assembly code cannot be analyzed by MIRAI.");
.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
12 changes: 6 additions & 6 deletions checker/src/body_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -309,7 +309,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
.cv
.session
.dcx()
.struct_span_warn(self.current_span, "The analysis of this function timed out");
.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 +1128,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 +1564,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 +1576,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 +2013,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 +2113,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 3d39f0e

Please sign in to comment.