Skip to content
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.

nightly-2023-12-30 #1272

Merged
merged 1 commit into from
Jul 16, 2024
Merged

nightly-2023-12-30 #1272

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file modified binaries/summary_store.tar
View file
Open in desktop
Binary file not shown.
55 changes: 33 additions & 22 deletions checker/src/block_visitor.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -365,7 +365,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
if !self.bv.cv.constant_time_tag_not_found {
self.bv.cv.constant_time_tag_not_found = true;
let span = self.bv.current_span;
let warning = self.bv.cv.session.struct_span_warn(
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
format!(
"unknown tag type for constant-time verification: {tag_name}",
Expand Down Expand Up @@ -960,7 +960,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.struct_span_warn(
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",
);
Expand Down Expand Up @@ -1025,7 +1025,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
}
match specialized_closure_ty.kind() {
TyKind::Closure(def_id, args)
| TyKind::Coroutine(def_id, args, _)
| TyKind::Coroutine(def_id, args)
| TyKind::FnDef(def_id, args) => {
return extract_func_ref(self.visit_function_reference(
*def_id,
Expand Down Expand Up @@ -1156,6 +1156,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.bv
.cv
.session
.dcx()
.struct_span_warn(span, diagnostic.as_ref().to_string());
for pc_span in precondition.spans.iter() {
let snippet = self.bv.tcx.sess.source_map().span_to_snippet(*pc_span);
Expand Down Expand Up @@ -1193,7 +1194,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
self.bv.post_condition_block = Some(this_block);
} else {
let span = self.bv.current_span;
let warning = self.bv.cv.session.struct_span_warn(
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
"multiple post conditions must be on the same execution path",
);
Expand Down Expand Up @@ -1232,7 +1233,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
let span = self.bv.current_span.source_callsite();
let message =
"this is unreachable, mark it as such by using the verify_unreachable! macro";
let warning = self.bv.cv.session.struct_span_warn(span, message);
let warning = self.bv.cv.session.dcx().struct_span_warn(span, message);
self.bv.emit_diagnostic(warning);
return None;
}
Expand All @@ -1249,7 +1250,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
} else {
"possible unsatisfied postcondition"
};
let warning = self.bv.cv.session.struct_span_warn(span, msg);
let warning = self.bv.cv.session.dcx().struct_span_warn(span, msg);
self.bv.emit_diagnostic(warning);
// Don't add the post condition to the summary
return None;
Expand All @@ -1269,6 +1270,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.bv
.cv
.session
.dcx()
.struct_span_warn(span, "provably false verification condition");
self.bv.emit_diagnostic(warning);
if entry_cond_as_bool.is_none()
Expand Down Expand Up @@ -1315,7 +1317,12 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
)
{
let span = self.bv.current_span.source_callsite();
let warning = self.bv.cv.session.struct_span_warn(span, warning.clone());
let warning = self
.bv
.cv
.session
.dcx()
.struct_span_warn(span, warning.clone());
self.bv.emit_diagnostic(warning);
}
}
Expand Down Expand Up @@ -1396,7 +1403,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
|| self.bv.preconditions.len() >= k_limits::MAX_INFERRED_PRECONDITIONS
{
let span = self.bv.current_span.source_callsite();
let warning = self.bv.cv.session.struct_span_warn(
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
format!(
"the {} {} have a {} tag",
Expand All @@ -1410,7 +1417,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
|| tag_check.extract_promotable_disjuncts(false).is_none()
{
let span = self.bv.current_span.source_callsite();
let warning = self.bv.cv.session.struct_span_warn(
let warning = self.bv.cv.session.dcx().struct_span_warn(
span,
format!(
"the {value_name} may have a {tag_name} tag, \
Expand All @@ -1426,11 +1433,11 @@ 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
.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!("the {value_name} has a {tag_name} tag"),
);
self.bv.emit_diagnostic(warning);
}

Expand Down Expand Up @@ -1536,8 +1543,12 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
if entry_cond_as_bool.unwrap_or(false) {
let error = get_assert_msg_description(msg);
let span = self.bv.current_span;
let warning =
self.bv.cv.session.struct_span_warn(span, error.to_string());
let warning = self
.bv
.cv
.session
.dcx()
.struct_span_warn(span, error.to_string());
self.bv.emit_diagnostic(warning);
// No need to push a precondition, the caller can never satisfy it.
return;
Expand Down Expand Up @@ -1571,7 +1582,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
// Can't make this the caller's problem.
let warning = format!("possible {}", get_assert_msg_description(msg));
let span = self.bv.current_span;
let warning = self.bv.cv.session.struct_span_warn(span, warning);
let warning = self.bv.cv.session.dcx().struct_span_warn(span, warning);
self.bv.emit_diagnostic(warning);
return;
}
Expand Down Expand Up @@ -1654,6 +1665,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
.bv
.cv
.session
.dcx()
.struct_span_warn(span, "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.
Expand Down Expand Up @@ -2589,7 +2601,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
}
}
mir::AggregateKind::Closure(def_id, args)
| mir::AggregateKind::Coroutine(def_id, args, _) => {
| mir::AggregateKind::Coroutine(def_id, args) => {
let ty = self.bv.tcx.type_of(*def_id).skip_binder();
let func_const = self.visit_function_reference(*def_id, ty, Some(args));
let func_val = Rc::new(func_const.clone().into());
Expand Down Expand Up @@ -3608,7 +3620,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
TyKind::Adt(adt_def, _) => adt_def
.discriminants(self.bv.tcx)
.find(|(_, var)| var.val == data),
TyKind::Coroutine(def_id, args, _) => {
TyKind::Coroutine(def_id, args) => {
let generator = args.as_coroutine();
generator
.discriminants(*def_id, self.bv.tcx)
Expand Down Expand Up @@ -3906,8 +3918,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
let len_path = Path::new_length(base_path.clone());
self.bv.update_value_at(len_path, len_val);
}
TyKind::Closure(def_id, generic_args)
| TyKind::Coroutine(def_id, generic_args, _) => {
TyKind::Closure(def_id, generic_args) | TyKind::Coroutine(def_id, generic_args) => {
let func_const = self.visit_function_reference(*def_id, ty, Some(generic_args));
let func_val = Rc::new(func_const.clone().into());
self.bv
Expand All @@ -3918,7 +3929,7 @@ impl<'block, 'analysis, 'compilation, 'tcx> BlockVisitor<'block, 'analysis, 'com
rustc_middle::ty::AliasTy { def_id, .. },
) => {
if let TyKind::Closure(def_id, generic_args)
| TyKind::Coroutine(def_id, generic_args, _) =
| TyKind::Coroutine(def_id, generic_args) =
self.bv.tcx.type_of(*def_id).skip_binder().kind()
{
let func_const =
Expand Down
15 changes: 10 additions & 5 deletions checker/src/body_visitor.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -309,6 +309,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
let warning = self
.cv
.session
.dcx()
.struct_span_warn(self.current_span, "The analysis of this function timed out");
self.emit_diagnostic(warning);
}
Expand Down Expand Up @@ -1130,7 +1131,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
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 warning = self.cv.session.struct_span_warn(span, message);
let warning = self.cv.session.dcx().struct_span_warn(span, message);
self.emit_diagnostic(warning);
}
}
Expand Down Expand Up @@ -1563,7 +1564,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
) = (old_layout, new_layout)
{
if *old_source == LayoutSource::DeAlloc {
let warning = self.cv.session.struct_span_warn(
let warning = self.cv.session.dcx().struct_span_warn(
self.current_span,
"the pointer points to memory that has already been deallocated",
);
Expand All @@ -1589,7 +1590,11 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
"deallocates"
}
);
let warning = self.cv.session.struct_span_warn(self.current_span, message);
let warning = self
.cv
.session
.dcx()
.struct_span_warn(self.current_span, message);
self.emit_diagnostic(warning);
}
}
Expand Down Expand Up @@ -2014,7 +2019,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
&self.type_visitor().generic_argument_map,
);
if source_field_index >= source_len {
let warning = self.cv.session.struct_span_warn(
let warning = self.cv.session.dcx().struct_span_warn(
self.current_span,
"The union is not fully initialized by this assignment",
);
Expand Down Expand Up @@ -2101,7 +2106,7 @@ impl<'analysis, 'compilation, 'tcx> BodyVisitor<'analysis, 'compilation, 'tcx> {
// Get another field
source_field_index += 1;
if source_field_index >= source_len {
let warning = self.cv.session.struct_span_warn(
let warning = self.cv.session.dcx().struct_span_warn(
self.current_span,
"The union is not fully initialized by this assignment",
);
Expand Down
Loading
Loading