From 3d39f0ec9e027334c8c1ac92aaeea43bf6671573 Mon Sep 17 00:00:00 2001 From: seanrion <45787907+seanrion@users.noreply.github.com> Date: Sat, 14 Dec 2024 14:11:59 +0800 Subject: [PATCH] Make MIRAI diagnostic message easier to identify --- checker/src/block_visitor.rs | 36 +++++++++++++++--------------- checker/src/body_visitor.rs | 12 +++++----- checker/src/call_visitor.rs | 32 +++++++++++++------------- checker/src/fixed_point_visitor.rs | 2 +- 4 files changed, 41 insertions(+), 41 deletions(-) diff --git a/checker/src/block_visitor.rs b/checker/src/block_visitor.rs index 3dd61b80..db21ec2f 100644 --- a/checker/src/block_visitor.rs +++ b/checker/src/block_visitor.rs @@ -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); @@ -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()], }; @@ -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); } @@ -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() { @@ -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); } @@ -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; @@ -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); @@ -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 @@ -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, @@ -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 @@ -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 @@ -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", ), @@ -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); } @@ -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 @@ -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; @@ -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); @@ -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(); diff --git a/checker/src/body_visitor.rs b/checker/src/body_visitor.rs index 0e2ce3d7..3bd49979 100644 --- a/checker/src/body_visitor.rs +++ b/checker/src/body_visitor.rs @@ -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!( @@ -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); } @@ -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); } @@ -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 { @@ -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; @@ -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; diff --git a/checker/src/call_visitor.rs b/checker/src/call_visitor.rs index 0e7e9272..3e5f3d8a 100644 --- a/checker/src/call_visitor.rs +++ b/checker/src/call_visitor.rs @@ -788,7 +788,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> if !entry_cond_as_bool.unwrap_or(true) { let span = self.block_visitor.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 .block_visitor .bv @@ -803,9 +803,9 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> // If the condition is always true, this assumption is redundant. If false, the // assumption is ignored. Otherwise, no diagnostics are emitted. let message = if cond_as_bool == Some(true) { - "assumption is provably true and can be deleted" + "[MIRAI] assumption is provably true and can be deleted" } else if cond_as_bool == Some(false) { - "assumption is provably false and it will be ignored" + "[MIRAI] assumption is provably false and it will be ignored" } else { return; }; @@ -948,7 +948,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> .cv .session .dcx() - .struct_span_warn(span, msg.to_string()); + .struct_span_warn(span, "[MIRAI] ".to_string()+&msg.to_string()); self.block_visitor.bv.emit_diagnostic(warning); } else { // If we see an unconditional panic inside a standard contract summary, @@ -974,7 +974,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> .cv .session .dcx() - .struct_span_warn(span, msg.to_string()); + .struct_span_warn(span, "[MIRAI] ".to_string()+&msg.to_string()); self.block_visitor.bv.emit_diagnostic(warning); } return; @@ -1023,7 +1023,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> .cv .session .dcx() - .struct_span_warn(span, msg.to_string()); + .struct_span_warn(span, "[MIRAI] ".to_string()+&msg.to_string()); self.block_visitor.bv.emit_diagnostic(warning); } else { // Since the assertion occurs in code that is being used rather than @@ -1099,7 +1099,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> let warning = self.block_visitor.bv.cv.session.dcx().struct_span_warn( self.block_visitor.bv.current_span, - warning.to_string(), + "[MIRAI] ".to_string()+&warning.to_string(), ); self.block_visitor.bv.emit_diagnostic(warning); } @@ -1448,7 +1448,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> if self.block_visitor.bv.check_for_errors && source_rustc_type.is_any_ptr() { let warning = self.block_visitor.bv.cv.session.dcx().struct_span_warn( self.block_visitor.bv.current_span, - "the macro add_tag! expects its argument to be a reference to a non-reference value", + "[MIRAI] the macro add_tag! expects its argument to be a reference to a non-reference value", ); self.block_visitor.bv.emit_diagnostic(warning); } @@ -1567,7 +1567,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> let warning = self.block_visitor.bv.cv.session.dcx().struct_span_warn( self.block_visitor.bv.current_span, format!( - "the macro {} expects its first argument to be a reference to a non-reference value", + "[MIRAI] the macro {} expects its first argument to be a reference to a non-reference value", if checking_presence { "has_tag! " } else { "does_not_have_tag!" }, ), ); @@ -1914,7 +1914,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> .cv .session .dcx() - .struct_span_warn(span, "preconditions should be reached unconditionally"); + .struct_span_warn(span, "[MIRAI] preconditions should be reached unconditionally"); self.block_visitor.bv.emit_diagnostic(warning); self.block_visitor.bv.check_for_unconditional_precondition = false; } @@ -2653,7 +2653,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> { let precondition = Precondition { condition: promotable_entry_condition.logical_not(), - message: Rc::from("incomplete analysis of call because of failure to resolve a nested call"), + message: Rc::from("[MIRAI] incomplete analysis of call because of failure to resolve a nested call"), provenance: None, spans: vec![self.block_visitor.bv.current_span.source_callsite()], }; @@ -2670,7 +2670,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> { let warning = self.block_visitor.bv.cv.session.dcx().struct_span_warn( self.block_visitor.bv.current_span, - "the called function could not be completely analyzed", + "[MIRAI] the called function could not be completely analyzed", ); self.block_visitor.bv.emit_diagnostic(warning); } @@ -3173,11 +3173,11 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> if self.block_visitor.bv.check_for_errors { let warning = self.block_visitor.bv.cv.session.dcx().struct_span_warn( self.block_visitor.bv.current_span, - "this argument should be a string literal, do not call this function directly", + "[MIRAI] this argument should be a string literal, do not call this function directly", ); self.block_visitor.bv.emit_diagnostic(warning); } - Rc::from("dummy argument") + Rc::from("[MIRAI] dummy argument") } /// Extract the tag kind and the propagation set from the generic arg of the function call @@ -3223,7 +3223,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> if self.block_visitor.bv.check_for_errors { let warning = self.block_visitor.bv.cv.session.dcx().struct_span_warn( self.block_visitor.bv.current_span, - "the tag type should be a generic type whose first parameter is a constant of type TagPropagationSet", + "[MIRAI] the tag type should be a generic type whose first parameter is a constant of type TagPropagationSet", ); self.block_visitor.bv.emit_diagnostic(warning); } @@ -3248,7 +3248,7 @@ impl<'call, 'block, 'analysis, 'compilation, 'tcx> if self.block_visitor.bv.check_for_errors { let warning = self.block_visitor.bv.cv.session.dcx().struct_span_warn( self.block_visitor.bv.current_span, - "the first parameter of the tag type should have type TagPropagationSet", + "[MIRAI] the first parameter of the tag type should have type TagPropagationSet", ); self.block_visitor.bv.emit_diagnostic(warning); } diff --git a/checker/src/fixed_point_visitor.rs b/checker/src/fixed_point_visitor.rs index 4e5ad672..afdc5f9c 100644 --- a/checker/src/fixed_point_visitor.rs +++ b/checker/src/fixed_point_visitor.rs @@ -164,7 +164,7 @@ impl<'fixed, 'analysis, 'compilation, 'tcx> let warning = self.bv.cv.session.dcx().struct_span_warn( span, format!( - "Fixed point loop iterations exceeded limit of {}", + "[MIRAI] Fixed point loop iterations exceeded limit of {}", k_limits::MAX_FIXPOINT_ITERATIONS ), );