Skip to content

Commit 3ca7510

Browse files
Use type_try_dynamic_cast
1 parent e513d02 commit 3ca7510

File tree

2 files changed

+30
-20
lines changed

2 files changed

+30
-20
lines changed

jbmc/src/java_bytecode/java_types.h

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -735,13 +735,23 @@ class java_generic_parametert : public reference_typet
735735
}
736736
};
737737

738+
/// Check whether a reference to a typet is a Java generic parameter/variable,
739+
/// e.g., `T` in `List<T>`.
740+
/// \param base: Source type.
741+
/// \return True if \p type is a generic Java parameter type
742+
template <>
743+
inline bool can_cast_type<java_generic_parametert>(const typet &base)
744+
{
745+
return is_reference(base) && is_java_generic_parameter_tag(base.subtype());
746+
}
747+
738748
/// Checks whether the type is a java generic parameter/variable, e.g., `T` in
739749
/// `List<T>`.
740750
/// \param type: the type to check
741751
/// \return true if type is a generic Java parameter type
742752
inline bool is_java_generic_parameter(const typet &type)
743753
{
744-
return is_reference(type) && is_java_generic_parameter_tag(type.subtype());
754+
return can_cast_type<java_generic_parametert>(type);
745755
}
746756

747757
/// \param type: source type

jbmc/src/java_bytecode/select_pointer_type.cpp

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -42,11 +42,10 @@ pointer_typet select_pointer_typet::specialize_generics(
4242
&generic_parameter_specialization_map,
4343
generic_parameter_recursion_trackingt &visited_nodes) const
4444
{
45-
if(is_java_generic_parameter(pointer_type))
45+
auto parameter = type_try_dynamic_cast<java_generic_parametert>(pointer_type);
46+
if(parameter != nullptr)
4647
{
47-
const java_generic_parametert &parameter =
48-
to_java_generic_parameter(pointer_type);
49-
const irep_idt &parameter_name = parameter.get_name();
48+
const irep_idt &parameter_name = parameter->get_name();
5049

5150
// avoid infinite recursion by looking at each generic argument from
5251
// previous assignments
@@ -82,26 +81,27 @@ pointer_typet select_pointer_typet::specialize_generics(
8281
visited_nodes.erase(parameter_name);
8382
return returned_type;
8483
}
85-
else if(pointer_type.subtype().id() == ID_struct_tag)
84+
85+
auto subtype =
86+
type_try_dynamic_cast<struct_tag_typet>(pointer_type.subtype());
87+
if(subtype != nullptr && is_java_array_tag(subtype->get_identifier()))
8688
{
8789
// if the pointer is an array, recursively specialize its element type
88-
const auto &array_subtype = to_struct_tag_type(pointer_type.subtype());
89-
if(is_java_array_tag(array_subtype.get_identifier()))
90+
const auto *array_element_type =
91+
type_try_dynamic_cast<pointer_typet>(java_array_element_type(*subtype));
92+
if(array_element_type != nullptr)
9093
{
91-
const typet &array_element_type = java_array_element_type(array_subtype);
92-
if(array_element_type.id() == ID_pointer)
93-
{
94-
const pointer_typet &new_array_type = specialize_generics(
95-
to_pointer_type(array_element_type),
96-
generic_parameter_specialization_map,
97-
visited_nodes);
98-
99-
pointer_typet replacement_array_type = java_array_type('a');
100-
replacement_array_type.subtype().set(ID_element_type, new_array_type);
101-
return replacement_array_type;
102-
}
94+
const pointer_typet &new_array_type = specialize_generics(
95+
*array_element_type,
96+
generic_parameter_specialization_map,
97+
visited_nodes);
98+
99+
pointer_typet replacement_array_type = java_array_type('a');
100+
replacement_array_type.subtype().set(ID_element_type, new_array_type);
101+
return replacement_array_type;
103102
}
104103
}
104+
105105
return pointer_type;
106106
}
107107

0 commit comments

Comments
 (0)