in checker/src/call_visitor.rs [2634:2845]
fn check_function_preconditions(&mut self, function_summary: &Summary) {
verify!(self.block_visitor.bv.check_for_errors);
// A precondition can refer to the result if the precondition prevents the result expression
// from overflowing.
let result = self
.destination
.map(|(r, _)| self.block_visitor.visit_rh_place(&r));
for precondition in &function_summary.preconditions {
let mut refined_condition = precondition.condition.refine_parameters_and_paths(
&self.actual_args,
&result,
&self.environment_before_call,
&self.block_visitor.bv.current_environment,
self.block_visitor.bv.fresh_variable_offset,
);
if self
.block_visitor
.bv
.current_environment
.entry_condition
.as_bool_if_known()
.is_none()
{
refined_condition = refined_condition.refine_with(
&self.block_visitor.bv.current_environment.entry_condition,
0,
);
}
let (refined_precondition_as_bool, entry_cond_as_bool) = self
.block_visitor
.bv
.check_condition_value_and_reachability(&refined_condition);
if refined_precondition_as_bool.unwrap_or(false) {
// The precondition is definitely true.
continue;
};
if !entry_cond_as_bool.unwrap_or(true) {
// The call is unreachable, so the precondition does not matter
continue;
}
if refined_condition.is_bottom() {
// The precondition has no value, assume it is unreachable after all.
debug!("precondition refines to BOTTOM {:?}", precondition);
continue;
}
let warn;
if !refined_precondition_as_bool.unwrap_or(true) {
// The precondition is definitely false.
if entry_cond_as_bool.unwrap_or(false)
&& self.block_visitor.bv.function_being_analyzed_is_root()
{
// We always get to this call and we are at the analysis root
self.issue_diagnostic_for_call(precondition, &refined_condition, false);
return;
} else {
// Promote the precondition, but be assertive.
// When the caller fails to meet the precondition, failure is certain.
warn = false;
}
} else {
warn = true;
}
// Is the precondition a tag check for a tag that flows from a subcomponent to the
// container?
if let Expression::UnknownTagCheck {
operand,
tag,
checking_presence,
} = &refined_condition.expression
{
if tag.is_propagated_by(TagPropagation::SuperComponent) {
// Look at sub components. If components that are located via
// pointers are tagged, those tags will not have propagated to here
// because the pointers are unidirectional.
if *checking_presence
&& operand.expression.has_tagged_subcomponent(
tag,
&self.block_visitor.bv.current_environment,
)
{
continue;
}
}
}
// If the current function is not an analysis root, promote the precondition, subject to a k-limit.
if (!self.block_visitor.bv.function_being_analyzed_is_root()
|| self.block_visitor.bv.cv.options.diag_level == DiagLevel::Default)
&& self.block_visitor.bv.preconditions.len() < k_limits::MAX_INFERRED_PRECONDITIONS
{
// Promote the callee precondition to a precondition of the current function.
// Unless, of course, if the precondition is already a precondition of the
// current function.
let seen_precondition = self.block_visitor.bv.preconditions.iter().any(|pc| {
pc.spans.last() == precondition.spans.last()
|| pc.provenance == precondition.provenance
});
if seen_precondition {
continue;
}
let promoted_condition = match (
self.block_visitor
.bv
.current_environment
.entry_condition
.extract_promotable_conjuncts(false),
refined_condition.extract_promotable_disjuncts(false),
) {
(Some(promotable_entry_condition), Some(promotable_condition)) => {
promotable_entry_condition
.logical_not()
.or(promotable_condition)
}
(Some(promotable_entry_condition), None) => {
if self.block_visitor.bv.cv.options.diag_level == DiagLevel::Default {
// If refined condition cannot be promoted, it may not be reasonable
// to require our caller to prove that this call can't be reached.
// Hence, we'll just leave the precondition un-promoted.
continue;
} else {
promotable_entry_condition.logical_not()
}
}
(None, Some(promotable_condition)) => promotable_condition,
_ => Rc::new(abstract_value::FALSE),
};
if promoted_condition.as_bool_if_known().is_none() {
if self.block_visitor.bv.current_span.in_derive_expansion() {
info!("derive macro has warning: {:?}", precondition.message);
// do not propagate preconditions across derive macros since
// derived code is pretty much foreign code.
continue;
}
if (self.block_visitor.bv.treat_as_foreign
|| !self.block_visitor.bv.def_id.is_local())
&& !matches!(
self.block_visitor.bv.cv.options.diag_level,
DiagLevel::Paranoid
)
&& precondition.message.contains("result unwrap failed")
{
// When foreign code unwraps a result, it is unlikely to be a parameter check.
// Instead, let's assume that the code intends a panic to happen if the
// result is not OK.
continue;
}
let mut stacked_spans = vec![self.block_visitor.bv.current_span];
stacked_spans.append(&mut precondition.spans.clone());
let promoted_precondition = Precondition {
condition: promoted_condition,
message: precondition.message.clone(),
provenance: precondition.provenance.clone(),
spans: stacked_spans,
};
self.block_visitor
.bv
.preconditions
.push(promoted_precondition);
continue;
} else if !refined_condition.as_bool_if_known().unwrap_or(true)
&& !self.block_visitor.bv.function_being_analyzed_is_root()
{
if let Some(true) = self
.block_visitor
.bv
.current_environment
.entry_condition
.as_bool_if_known()
{
// Just a pass through function
let mut promoted_precondition = precondition.clone();
promoted_precondition.condition = refined_condition;
self.block_visitor
.bv
.preconditions
.push(promoted_precondition);
continue;
}
}
}
// The precondition cannot be promoted, so the buck stops here.
if precondition
.message
.starts_with("incomplete analysis of call")
{
// If the precondition is not satisfied, the summary of the callee is incomplete
// and so should be the summary of this method.
self.block_visitor.bv.analysis_is_incomplete = true;
if self.block_visitor.bv.cv.options.diag_level == DiagLevel::Default {
// Don't give a diagnostic in default mode, since it is hard for casual users
// to do something about missing/incomplete summaries.
continue;
}
}
if self.block_visitor.bv.cv.options.diag_level == DiagLevel::Default
&& refined_condition.expression.contains_top()
{
// If the refined precondition contains TOP expressions, precision has
// been lost and the message is more likely than not a false positive.
continue;
}
self.issue_diagnostic_for_call(precondition, &refined_condition, warn);
}
}