in checker/src/call_visitor.rs [1021:1153]
fn try_to_inline_special_function(&mut self) -> Rc<AbstractValue> {
match self.callee_known_name {
KnownNames::RustAlloc => self.handle_rust_alloc(),
KnownNames::RustAllocZeroed => self.handle_rust_alloc_zeroed(),
KnownNames::RustRealloc => self.handle_rust_realloc(),
KnownNames::StdIntrinsicsArithOffset => self.handle_arith_offset(),
KnownNames::StdIntrinsicsBitreverse
| KnownNames::StdIntrinsicsBswap
| KnownNames::StdIntrinsicsCtlz
| KnownNames::StdIntrinsicsCtpop
| KnownNames::StdIntrinsicsCttz => {
checked_assume!(self.actual_args.len() == 1);
let arg_type = ExpressionType::from(self.actual_argument_types[0].kind());
let bit_length = arg_type.bit_length();
self.actual_args[0]
.1
.intrinsic_bit_vector_unary(bit_length, self.callee_known_name)
}
KnownNames::StdIntrinsicsCtlzNonzero | KnownNames::StdIntrinsicsCttzNonzero => {
checked_assume!(self.actual_args.len() == 1);
if self.block_visitor.bv.check_for_errors {
let non_zero = self.actual_args[0].1.not_equals(Rc::new(0u128.into()));
if let Some(warning) = self.block_visitor.check_special_function_condition(
&non_zero,
"argument is zero",
self.callee_known_name,
) {
// The condition may be reachable and false. Promote it to a precondition if possible.
match (
self.block_visitor
.bv
.current_environment
.entry_condition
.extract_promotable_conjuncts(false),
non_zero.extract_promotable_disjuncts(false),
) {
(Some(promotable_entry_condition), Some(promotable_non_zero))
if self.block_visitor.bv.preconditions.len()
< k_limits::MAX_INFERRED_PRECONDITIONS =>
{
let condition = promotable_entry_condition
.logical_not()
.or(promotable_non_zero);
let precondition = Precondition {
condition,
message: warning,
provenance: None,
spans: vec![self.block_visitor.bv.current_span],
};
self.block_visitor.bv.preconditions.push(precondition);
}
_ => {
let warning = self.block_visitor.bv.cv.session.struct_span_warn(
self.block_visitor.bv.current_span,
warning.as_ref(),
);
self.block_visitor.bv.emit_diagnostic(warning);
}
}
}
}
let arg_type = ExpressionType::from(self.actual_argument_types[0].kind());
let bit_length = arg_type.bit_length();
self.actual_args[0]
.1
.intrinsic_bit_vector_unary(bit_length, self.callee_known_name)
}
KnownNames::StdIntrinsicsCeilf32
| KnownNames::StdIntrinsicsCeilf64
| KnownNames::StdIntrinsicsCosf32
| KnownNames::StdIntrinsicsCosf64
| KnownNames::StdIntrinsicsExp2f32
| KnownNames::StdIntrinsicsExp2f64
| KnownNames::StdIntrinsicsExpf32
| KnownNames::StdIntrinsicsExpf64
| KnownNames::StdIntrinsicsFabsf32
| KnownNames::StdIntrinsicsFabsf64
| KnownNames::StdIntrinsicsFloorf32
| KnownNames::StdIntrinsicsFloorf64
| KnownNames::StdIntrinsicsLog10f32
| KnownNames::StdIntrinsicsLog10f64
| KnownNames::StdIntrinsicsLog2f32
| KnownNames::StdIntrinsicsLog2f64
| KnownNames::StdIntrinsicsLogf32
| KnownNames::StdIntrinsicsLogf64
| KnownNames::StdIntrinsicsNearbyintf32
| KnownNames::StdIntrinsicsNearbyintf64
| KnownNames::StdIntrinsicsRintf32
| KnownNames::StdIntrinsicsRintf64
| KnownNames::StdIntrinsicsRoundf32
| KnownNames::StdIntrinsicsRoundf64
| KnownNames::StdIntrinsicsSinf32
| KnownNames::StdIntrinsicsSinf64
| KnownNames::StdIntrinsicsSqrtf32
| KnownNames::StdIntrinsicsSqrtf64
| KnownNames::StdIntrinsicsTruncf32
| KnownNames::StdIntrinsicsTruncf64 => {
checked_assume!(self.actual_args.len() == 1);
self.actual_args[0]
.1
.intrinsic_floating_point_unary(self.callee_known_name)
}
KnownNames::StdIntrinsicsCopysignf32
| KnownNames::StdIntrinsicsCopysignf64
| KnownNames::StdIntrinsicsFaddFast
| KnownNames::StdIntrinsicsFdivFast
| KnownNames::StdIntrinsicsFmulFast
| KnownNames::StdIntrinsicsFremFast
| KnownNames::StdIntrinsicsFsubFast
| KnownNames::StdIntrinsicsMaxnumf32
| KnownNames::StdIntrinsicsMaxnumf64
| KnownNames::StdIntrinsicsMinnumf32
| KnownNames::StdIntrinsicsMinnumf64
| KnownNames::StdIntrinsicsPowf32
| KnownNames::StdIntrinsicsPowf64
| KnownNames::StdIntrinsicsPowif32
| KnownNames::StdIntrinsicsPowif64 => {
checked_assume!(self.actual_args.len() == 2);
self.actual_args[0]
.1
.intrinsic_binary(self.actual_args[1].1.clone(), self.callee_known_name)
}
KnownNames::StdIntrinsicsMinAlignOfVal => self.handle_min_align_of_val(),
KnownNames::StdIntrinsicsMulWithOverflow => self.handle_checked_binary_operation(),
KnownNames::StdIntrinsicsNeedsDrop => self.handle_needs_drop(),
KnownNames::StdIntrinsicsOffset => self.handle_offset(),
KnownNames::StdIntrinsicsRawEq => self.handle_raw_eq(),
KnownNames::StdIntrinsicsSizeOf => self.handle_size_of(),
KnownNames::StdIntrinsicsSizeOfVal => self.handle_size_of_val(),
KnownNames::StdSliceCmpMemcmp => self.handle_memcmp(),
_ => abstract_value::BOTTOM.into(),
}
}