in checker/src/call_visitor.rs [1458:1618]
fn handle_check_tag(&mut self, checking_presence: bool) {
precondition!(self.actual_args.len() == 1);
let result: Option<Rc<AbstractValue>>;
if let Some(tag) = self.extract_tag_kind_and_propagation_set() {
let (source_path, source_rustc_type) = self.deref_tag_source();
trace!(
"MiraiCheckTag: checking if {:?} has {}been tagged with {:?}",
source_path,
(if checking_presence { "" } else { "never " }),
tag,
);
// Check if the tagged value has a pointer type (e.g., a reference).
// Emit a warning message if so.
if self.block_visitor.bv.check_for_errors && source_rustc_type.is_any_ptr() {
let warning = self.block_visitor.bv.cv.session.struct_span_warn(
self.block_visitor.bv.current_span,
format!(
"the macro {} expects its first argument to be a reference to a non-reference value",
if checking_presence { "has_tag! " } else { "does_not_have_tag!" },
).as_str(),
);
self.block_visitor.bv.emit_diagnostic(warning);
}
// Get the value to check for the presence or absence of the tag
let (tag_field_path, tag_field_value) = self.get_value_to_check_for_tag(
tag,
checking_presence,
source_path.clone(),
source_rustc_type,
);
// Decide the result of has_tag! or does_not_have_tag!.
let mut check_result =
AbstractValue::make_tag_check(tag_field_value, tag, checking_presence);
// If the tag can be propagated through sub-components we need to check the tag on the
// values that can contain tag_field_path as a sub-component.
// Operationally, if tag_field_path is a qualified path we check if any of its prefixes
// has the tag (when checking_presence = true), or if all of its prefixes does not have
// the tag (when checking_presence = false).
if tag.is_propagated_by(TagPropagation::SubComponent) {
let mut path_prefix = &tag_field_path;
while let PathEnum::QualifiedPath { qualifier, .. } = &path_prefix.value {
path_prefix = qualifier;
let path_prefix_rustc_type = self
.type_visitor()
.get_path_rustc_type(path_prefix, self.block_visitor.bv.current_span);
if !path_prefix_rustc_type.is_scalar() {
let tag_field_value = self
.block_visitor
.bv
.extract_tag_field_of_non_scalar_value_at(
path_prefix,
path_prefix_rustc_type,
)
.1;
if checking_presence {
// We are checking presence of a tag. It is equivalent to *any* prefix having the tag.
// Thus we use a logical or.
check_result = check_result.or(AbstractValue::make_tag_check(
tag_field_value,
tag,
checking_presence,
));
// Exits the loop if check_result is already true.
if check_result.as_bool_if_known().unwrap_or(false) {
break;
}
} else {
// We are checking absence of a tag. It is equivalent to *all* prefixes not having the tag.
// Thus we use a logical and.
check_result = check_result.and(AbstractValue::make_tag_check(
tag_field_value,
tag,
checking_presence,
));
// Exits the loop if check_result is already false.
if !check_result.as_bool_if_known().unwrap_or(true) {
break;
}
}
}
}
}
// If the tag can be propagated from a sub-component to its container
if tag.is_propagated_by(TagPropagation::SuperComponent) {
let root = source_path.get_path_root();
let value_map = self.block_visitor.bv.current_environment.value_map.clone();
for (_, value) in value_map.iter().filter(|(p, _)| p.is_rooted_by(root)) {
let mut value = value.clone();
if let Expression::Reference(p) = &value.expression {
if let PathEnum::HeapBlock { .. } = &p.value {
let layout_field = Path::new_layout(p.clone());
let (_, tag_field_value) = self
.block_visitor
.bv
.extract_tag_field_of_non_scalar_value_at(
&layout_field,
self.block_visitor.bv.tcx.types.trait_object_dummy_self,
);
value = tag_field_value.clone();
}
}
if checking_presence {
// We are checking presence of a tag. It is equivalent to *any* prefix having the tag.
// Thus we use a logical or.
check_result = check_result.or(AbstractValue::make_tag_check(
value,
tag,
checking_presence,
));
// Exits the loop if check_result is already true.
if check_result.as_bool_if_known().unwrap_or(false) {
break;
}
} else {
// We are checking absence of a tag. It is equivalent to *all* prefixes not having the tag.
// Thus we use a logical and.
check_result = check_result.and(AbstractValue::make_tag_check(
value,
tag,
checking_presence,
));
// Exits the loop if check_result is already false.
if !check_result.as_bool_if_known().unwrap_or(true) {
break;
}
}
}
}
result = Some(check_result);
} else {
result = None;
}
// Return the abstract result and update exit conditions.
let destination = &self.destination;
if let Some((place, _)) = destination {
let target_path = self.block_visitor.visit_rh_place(place);
self.block_visitor.bv.update_value_at(
target_path.clone(),
result.unwrap_or_else(|| {
AbstractValue::make_typed_unknown(ExpressionType::Bool, target_path)
}),
);
} else {
assume_unreachable!("expected the function call has a destination");
}
self.use_entry_condition_as_exit_condition();
}