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

Commit

Permalink
nightly-2023-12-30 (#1272)
Browse files Browse the repository at this point in the history
  • Loading branch information
@hermanventer
hermanventer committed Jul 16, 2024
1 parent f432804 commit 41887ea
Show file tree
Hide file tree
Showing 26 changed files with 110 additions and 89 deletions.
Binary file modified binaries/summary_store.tar
View file
Binary file not shown.
55 changes: 33 additions & 22 deletions checker/src/block_visitor.rs
View file
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
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

0 comments on commit 41887ea

Please sign in to comment.