in checker/src/call_visitor.rs [755:1012]
fn report_calls_to_special_functions(&mut self) {
precondition!(self.block_visitor.bv.check_for_errors);
match self.callee_known_name {
KnownNames::MiraiAssume => {
assume!(self.actual_args.len() == 1);
let (_, cond) = &self.actual_args[0];
let (cond_as_bool, entry_cond_as_bool) = self
.block_visitor
.bv
.check_condition_value_and_reachability(cond);
// If we never get here, rather call verify_unreachable!()
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";
let warning = self
.block_visitor
.bv
.cv
.session
.struct_span_warn(span, message);
self.block_visitor.bv.emit_diagnostic(warning);
return;
}
// 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"
} else if cond_as_bool == Some(false) {
"assumption is provably false and it will be ignored"
} else {
return;
};
let span = self.block_visitor.bv.current_span.source_callsite();
let warning = self
.block_visitor
.bv
.cv
.session
.struct_span_warn(span, message);
self.block_visitor.bv.emit_diagnostic(warning);
}
KnownNames::MiraiPostcondition => {
let actual_args = self.actual_args.clone();
assume!(actual_args.len() == 3); // The type checker ensures this.
let (_, assumption) = &actual_args[1];
let (_, cond) = &actual_args[0];
if !assumption.as_bool_if_known().unwrap_or(false) {
// Not an assumed post condition, so check the condition and only add this to
// the summary if it is reachable and true.
let message = self.coerce_to_string(&actual_args[2].0.clone());
if self
.block_visitor
.check_special_function_condition(
cond,
message.as_ref(),
KnownNames::MiraiPostcondition,
)
.is_none()
{
self.block_visitor.try_extend_post_condition(cond);
}
} else {
self.block_visitor.try_extend_post_condition(cond);
}
}
KnownNames::MiraiVerify => {
let actual_args = self.actual_args.clone();
assume!(actual_args.len() == 2); // The type checker ensures this.
let (_, cond) = &actual_args[0];
let message = self.coerce_to_string(&actual_args[1].0);
self.block_visitor.check_special_function_condition(
cond,
message.as_ref(),
KnownNames::MiraiVerify,
);
}
KnownNames::StdPanickingAssertFailed
| KnownNames::StdPanickingBeginPanic
| KnownNames::StdPanickingBeginPanicFmt => {
assume!(!self.actual_args.is_empty()); // The type checker ensures this.
let mut path_cond = self.block_visitor.might_be_reachable();
if !path_cond.unwrap_or(true) {
// We never get to this call, so nothing to report.
return;
}
let msg = match self.callee_known_name {
KnownNames::StdPanickingAssertFailed => Rc::from("assertion failed"),
KnownNames::StdPanickingBeginPanic => {
self.coerce_to_string(&self.actual_args[0].0.clone())
}
_ => {
let arguments_struct_path = self.actual_args[0].0.clone();
let pieces_path_fat = Path::new_field(arguments_struct_path.clone(), 0)
.canonicalize(&self.block_visitor.bv.current_environment);
let pieces_path_thin = Path::new_field(pieces_path_fat.clone(), 0);
let pieces_path_len = Path::new_length(pieces_path_fat);
let len_val = self.block_visitor.bv.lookup_path_and_refine_result(
pieces_path_len,
self.block_visitor.bv.tcx.types.usize,
);
let len = if let Expression::CompileTimeConstant(ConstantDomain::U128(v)) =
&len_val.expression
{
*v
} else {
1u128
};
let args_path_fat = Path::new_field(arguments_struct_path, 2)
.canonicalize(&self.block_visitor.bv.current_environment);
let args_path_len = Path::new_length(args_path_fat);
let arg_len_val = self.block_visitor.bv.lookup_path_and_refine_result(
args_path_len,
self.block_visitor.bv.tcx.types.usize,
);
let num_args =
if let Expression::CompileTimeConstant(ConstantDomain::U128(v)) =
&arg_len_val.expression
{
*v
} else {
1u128
};
let mut msg = String::new();
for i in 0..len {
let index = Rc::new(i.into());
let piece_path_fat = Path::new_index(pieces_path_thin.clone(), index)
.canonicalize(&self.block_visitor.bv.current_environment);
msg += self.coerce_to_string(&piece_path_fat).as_ref();
if i < num_args {
msg += "{}";
// todo: attach arg value to precondition and let caller refine them
// and turn them into strings suitable for display in the diagnostics
}
}
Rc::from(msg)
}
};
if msg.contains("entered unreachable code")
|| msg.contains("not yet implemented")
|| msg.contains("not implemented")
|| msg.starts_with("unrecoverable: ")
|| (msg.starts_with("assertion failed")
&& self.block_visitor.bv.cv.options.test_only)
{
// We treat unreachable!() as an assumption rather than an assertion to prove.
// unimplemented!() is unlikely to be a programmer mistake, so need to fixate on that either.
// unrecoverable! is way for the programmer to indicate that termination is not a mistake.
return;
} else if path_cond.is_none() && msg.as_ref() == "statement is reachable" {
// verify_unreachable should always complain if possibly reachable
// and the current function is public or root.
path_cond = Some(true);
};
let span = self.block_visitor.bv.current_span.source_callsite();
if path_cond.unwrap_or(false)
&& self.block_visitor.bv.function_being_analyzed_is_root()
{
// We always get to this call and we have to assume that the function will
// get called, so keep the message certain.
// Don't, however, complain about panics in the standard contract summaries
if std::env::var("MIRAI_START_FRESH").is_err() {
let warning = self
.block_visitor
.bv
.cv
.session
.struct_span_warn(span, msg.as_ref());
self.block_visitor.bv.emit_diagnostic(warning);
} else {
// If we see an unconditional panic inside a standard contract summary,
// make it into an unsatisfiable precondition.
let precondition = Precondition {
condition: Rc::new(abstract_value::FALSE),
message: msg,
provenance: None,
spans: vec![],
};
self.block_visitor.bv.preconditions.push(precondition);
}
} else {
// We might get to this call, depending on the state at the call site.
//
if msg.contains("Post-condition of ") || msg.contains("Invariant of ") {
// Dealing with contracts crate
if self.block_visitor.bv.function_being_analyzed_is_root() {
let msg = msg.replace(" violated", " possibly violated");
let warning = self
.block_visitor
.bv
.cv
.session
.struct_span_warn(span, msg.as_ref());
self.block_visitor.bv.emit_diagnostic(warning);
}
return;
}
// In the case when an assert macro has been called, the inverse of the assertion
// was conjoined into the entry condition and this condition was simplified.
// We therefore cannot distinguish the case of maybe reaching a definitely
// false assertion from the case of definitely reaching a maybe false assertion.
//
// Since the assert and panic macros are commonly used to create preconditions
// it would be very inconvenient if this possibly false assertion were reported
// as a problem since there would be no way to shut it up. We therefore do not
// report this and instead insist that anyone who wants to have MIRAI check
// their assertions should use the mirai_annotations::verify! macro instead.
//
// We **do** have to push a precondition since this is the probable intent.
if let Some(promotable_entry_condition) = self
.block_visitor
.bv
.current_environment
.entry_condition
.extract_promotable_conjuncts(false)
{
let condition = promotable_entry_condition.logical_not();
let precondition = Precondition {
condition,
message: msg,
provenance: None,
spans: if self.block_visitor.bv.def_id.is_local() {
vec![span]
} else {
vec![] // The span is likely inside a standard macro, i.e. panic! etc.
},
};
self.block_visitor.bv.preconditions.push(precondition);
} else {
// If the assertion cannot be promoted because the caller cannot
// satisfy it (because it contains a reference to local variable),
// then we need to produce a diagnostic after all, but only if this
// a local function (i.e. a function in the crate being analyzed).
if self.block_visitor.bv.def_id.is_local() {
let warning = self
.block_visitor
.bv
.cv
.session
.struct_span_warn(span, msg.as_ref());
self.block_visitor.bv.emit_diagnostic(warning);
} else {
// Since the assertion occurs in code that is being used rather than
// analyzed, we'll assume that the code is correct and the analyzer
// discovered a false positive.
}
}
}
}
_ => assume_unreachable!(),
}
}