Skip to content

[TG-7815] Fix bug in get_recursively_instantiated_type #4913

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 5 commits into from
Closed

[TG-7815] Fix bug in get_recursively_instantiated_type #4913

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
4abbd7a
Added ability to output generic_parameter_specialization_mapt
NathanJPhillips Jul 11, 2019
cf6d6fb
Fixed implementation of get_recursively_instantiated_type
NathanJPhillips Jul 11, 2019
e4b7363
Use type_try_dynamic_cast
NathanJPhillips Jul 15, 2019
8125a9f
Remove simplistic method that assumes no recursion
NathanJPhillips Jul 15, 2019
ec69b1b
Avoid repeating check that will be done in called function
NathanJPhillips Jul 15, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
119 changes: 38 additions & 81 deletions jbmc/src/java_bytecode/select_pointer_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,61 +25,60 @@ pointer_typet select_pointer_typet::convert_pointer_type(
// a generic parameter, specialize it with concrete types
if(!generic_parameter_specialization_map.empty())
{
generic_parameter_recursion_trackingt visited;
const auto &type = specialize_generics(
pointer_type, generic_parameter_specialization_map, visited);
INVARIANT(visited.empty(), "recursion stack must be empty here");
return type;
return specialize_generics(
pointer_type, generic_parameter_specialization_map);
}
else
{
return pointer_type;
}
}

/// Return the first concrete type instantiation if any such exists.
///
/// Example:
/// `class MyGeneric<T,U> { MyGeneric<U,T> gen; T t;}`
/// When instantiating `MyGeneric<Integer,String> my` we need to for example
/// resolve the type of `my.gen.t`. The map would in this context contain
/// - T -> (Integer, U)
/// - U -> (String, T)
///
/// Note that the top of the stacks for T and U create a recursion T -> U,
/// U-> T. We want to break it and specialize `T my.gen.t` to `String my.gen.t`.
/// \param pointer_type: The pointer type to specialize
/// \param generic_parameter_specialization_map: Map of type names to
/// specialization stack
/// \return The first instantiated type for the generic type or nothing if no
/// such instantiation exists.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be updated slightly - it sounds l like it's only handling the recursion case (because it's just moved from the function that was breaking recursion). Also, move the documentation to the header.

pointer_typet select_pointer_typet::specialize_generics(
const pointer_typet &pointer_type,
const generic_parameter_specialization_mapt
&generic_parameter_specialization_map,
generic_parameter_recursion_trackingt &visited_nodes) const
&generic_parameter_specialization_map) const
{
auto parameter = type_try_dynamic_cast<java_generic_parametert>(pointer_type);
if(parameter != nullptr)
{
const irep_idt &parameter_name = parameter->get_name();
irep_idt parameter_name = parameter->get_name();

// avoid infinite recursion by looking at each generic argument from
// previous assignments
if(visited_nodes.find(parameter_name) != visited_nodes.end())
generic_parameter_specialization_mapt spec_map_copy =
generic_parameter_specialization_map;
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 You're making a copy of the map over and over again, changing a single element in it in each call. I don't have any good idea how to make this less costly though.. not so nice ideas being keeping two functions, make the code uglier at the call site, or add extra arguments to the function (depth of each stack to look at). Can you think of a better way?

while(true)
{
const optionalt<pointer_typet> result = get_recursively_instantiated_type(
parameter_name, generic_parameter_specialization_map);
return result.has_value() ? result.value() : pointer_type;
auto types_it = spec_map_copy.find(parameter_name);
if(types_it == spec_map_copy.end() || types_it->second.empty())
{
// This means that the generic pointer_type has not been specialized
// in the current context (e.g., the method under test is generic);
// we return the pointer_type itself which is a pointer to its upper
// bound
return pointer_type;
}
const reference_typet &type = types_it->second.back();
types_it->second.pop_back();
if(!is_java_generic_parameter(type))
return type;
parameter_name = to_java_generic_parameter(type).get_name();
}

if(generic_parameter_specialization_map.count(parameter_name) == 0)
{
// this means that the generic pointer_type has not been specialized
// in the current context (e.g., the method under test is generic);
// we return the pointer_type itself which is basically a pointer to
// its upper bound
return pointer_type;
}
const pointer_typet &type =
generic_parameter_specialization_map.find(parameter_name)->second.back();

// generic parameters can be adopted from outer classes or superclasses so
// we may need to search for the concrete type recursively
if(!is_java_generic_parameter(type))
return type;

visited_nodes.insert(parameter_name);
const auto returned_type = specialize_generics(
to_java_generic_parameter(type),
generic_parameter_specialization_map,
visited_nodes);
visited_nodes.erase(parameter_name);
return returned_type;
}

auto subtype =
Expand All @@ -94,8 +93,7 @@ pointer_typet select_pointer_typet::specialize_generics(

const pointer_typet &new_array_type = specialize_generics(
*array_element_type,
generic_parameter_specialization_map,
visited_nodes);
generic_parameter_specialization_map);

pointer_typet replacement_array_type = java_array_type('a');
replacement_array_type.subtype().set(ID_element_type, new_array_type);
Expand All @@ -105,47 +103,6 @@ pointer_typet select_pointer_typet::specialize_generics(
return pointer_type;
}

/// Return the first concrete type instantiation if any such exists. This method
/// is only to be called when \ref select_pointer_typet::specialize_generics
/// cannot find an instantiation due to a loop in its recursion.
///
/// Example:
/// `class MyGeneric<T,U> { MyGeneric<U,T> gen; T t;}`
/// When instantiating `MyGeneric<Integer,String> my` we need to for example
/// resolve the type of `my.gen.t`. The map would in this context contain
/// - T -> (Integer, U)
/// - U -> (String, T)
///
/// Note that the top of the stacks for T and U create a recursion T -> U,
/// U-> T. We want to break it and specialize `T my.gen.t` to `String my.gen.t`.
/// \param parameter_name: The name of the generic parameter type we want to
/// have instantiated
/// \param generic_parameter_specialization_map: Map of type names to
/// specialization stack
/// \return The first instantiated type for the generic type or nothing if no
/// such instantiation exists.
optionalt<pointer_typet>
select_pointer_typet::get_recursively_instantiated_type(
irep_idt parameter_name,
generic_parameter_specialization_mapt
generic_parameter_specialization_map) const
{
while(true)
{
auto types_it = generic_parameter_specialization_map.find(parameter_name);
INVARIANT(
types_it != generic_parameter_specialization_map.end(),
"Type parameter must have a type argument");
if(types_it->second.empty())
return {};
reference_typet type = types_it->second.back();
types_it->second.pop_back();
if(!is_java_generic_parameter(type))
return std::move(type);
parameter_name = to_java_generic_parameter(type).get_name();
}
}

std::set<struct_tag_typet>
select_pointer_typet::get_parameter_alternative_types(
const irep_idt &,
Expand Down
9 changes: 1 addition & 8 deletions jbmc/src/java_bytecode/select_pointer_type.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ Author: Diffblue Ltd.

typedef std::unordered_map<irep_idt, std::vector<reference_typet>>
generic_parameter_specialization_mapt;
typedef std::set<irep_idt> generic_parameter_recursion_trackingt;

struct print_generic_parameter_specialization_map
{
Expand Down Expand Up @@ -54,11 +53,6 @@ class namespacet;

class select_pointer_typet
{
optionalt<pointer_typet> get_recursively_instantiated_type(
irep_idt parameter_name,
generic_parameter_specialization_mapt
generic_parameter_specialization_map) const;

public:
virtual ~select_pointer_typet() = default;

Expand Down Expand Up @@ -111,8 +105,7 @@ class select_pointer_typet
pointer_typet specialize_generics(
const pointer_typet &pointer_type,
const generic_parameter_specialization_mapt
&generic_parameter_specialization_map,
generic_parameter_recursion_trackingt &visited_nodes) const;
&generic_parameter_specialization_map) const;
};

#endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H