in checker/src/block_visitor.rs [1422:1557]
fn visit_assert(
&mut self,
cond: &mir::Operand<'tcx>,
expected: bool,
msg: &mir::AssertMessage<'tcx>,
target: mir::BasicBlock,
cleanup: Option<mir::BasicBlock>,
) {
// Propagate the entry condition to the successor blocks, conjoined with cond (or !cond).
let cond_val = self.visit_operand(cond);
let not_cond_val = cond_val.logical_not();
if let Some(cleanup_target) = cleanup {
let panic_exit_condition =
self.bv
.current_environment
.entry_condition
.and(if expected {
not_cond_val.clone()
} else {
cond_val.clone()
});
if !panic_exit_condition.is_bottom() {
self.bv
.current_environment
.exit_conditions
.insert_mut(cleanup_target, panic_exit_condition);
}
};
let normal_exit_condition = self
.bv
.current_environment
.entry_condition
.and(if expected {
cond_val.clone()
} else {
not_cond_val
});
if !normal_exit_condition.is_bottom() {
self.bv
.current_environment
.exit_conditions
.insert_mut(target, normal_exit_condition);
// Check the condition and issue a warning or infer a precondition.
if self.bv.check_for_errors {
if let mir::Operand::Constant(..) = cond {
// Do not complain about compile time constants known to the compiler.
// Leave that to the compiler.
} else {
let (cond_as_bool_opt, entry_cond_as_bool) =
self.bv.check_condition_value_and_reachability(&cond_val);
// Quick exit if things are known.
if let Some(false) = entry_cond_as_bool {
// We can't reach this assertion, so just return.
return;
}
if let Some(cond_as_bool) = cond_as_bool_opt {
if expected == cond_as_bool {
// If the condition is always as expected when we get here, so there is nothing to report.
return;
}
// The condition is known to differ from expected so if we always get here if called,
// emit a diagnostic.
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);
self.bv.emit_diagnostic(warning);
// No need to push a precondition, the caller can never satisfy it.
return;
}
}
// At this point, we don't know that this assert is unreachable and we don't know
// that the condition is as expected, so we need to warn about it somewhere.
check_for_early_return!(self.bv);
let promotable_cond_val = cond_val.extract_promotable_disjuncts(false);
check_for_early_return!(self.bv);
let promotable_entry_cond = self
.bv
.current_environment
.entry_condition
.extract_promotable_conjuncts(false);
if promotable_cond_val.is_none()
|| promotable_entry_cond.is_none()
|| self.bv.preconditions.len() >= k_limits::MAX_INFERRED_PRECONDITIONS
|| (self.bv.function_being_analyzed_is_root()
&& 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 span = self.bv.current_span;
let warning = self.bv.cv.session.struct_span_warn(span, warning.as_str());
self.bv.emit_diagnostic(warning);
return;
}
// Make it the caller's problem by pushing a precondition.
// After, of course, removing any promoted preconditions that match the current
// source span.
let sp = self.bv.current_span;
self.bv
.preconditions
.retain(|pc| pc.spans.last() != Some(&sp));
let expected_cond = if expected {
promotable_cond_val.unwrap()
} else {
promotable_cond_val.unwrap().logical_not()
};
// To make sure that this assertion never fails, we should either never
// get here (!entry_condition) or expected_cond should be true.
let condition = promotable_entry_cond
.unwrap()
.logical_not()
.or(expected_cond);
let message = Rc::from(String::from(get_assert_msg_description(msg)));
let precondition = Precondition {
condition,
message,
provenance: None,
spans: vec![self.bv.current_span],
};
self.bv.preconditions.push(precondition);
}
}
}
fn get_assert_msg_description<'tcx>(msg: &mir::AssertMessage<'tcx>) -> &'tcx str {
match msg {
mir::AssertKind::BoundsCheck { .. } => "index out of bounds",
_ => msg.description(),
}
}
}