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 2 commits
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
92 changes: 15 additions & 77 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 @@ -126,86 +126,24 @@ pointer_typet select_pointer_typet::specialize_generics(
/// 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.

optionalt<pointer_typet>
select_pointer_typet::get_recursively_instantiated_type(
const irep_idt &parameter_name,
const generic_parameter_specialization_mapt
&generic_parameter_specialization_map) const
irep_idt parameter_name,
generic_parameter_specialization_mapt
generic_parameter_specialization_map) const
{
generic_parameter_recursion_trackingt visited;
const size_t max_depth =
generic_parameter_specialization_map.find(parameter_name)->second.size();

irep_idt current_parameter = parameter_name;
for(size_t depth = 0; depth < max_depth; depth++)
while(true)
Copy link
Contributor

Choose a reason for hiding this comment

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

Looks good, but since taking a map by value like this is quite unusual please add comments noting the strategy you're using here and why

Copy link
Contributor

Choose a reason for hiding this comment

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

The map itself is not taken by value. I don't think we need to document why passing a struct by value is OK.

Copy link

Choose a reason for hiding this comment

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

I'm not sure what you mean by "not taken by value". We do make a copy here, so we can pop from the stacks of particular parameters in the map just for the sake of finding the parameter specialization, but at the call site of this function we need to keep the original full information. I agree that adding a note that points this out is useful (not arguing why it's ok, just to make the reader notice), I missed it myself at first.

{
const auto retval = get_recursively_instantiated_type(
current_parameter, generic_parameter_specialization_map, visited, depth);
if(retval.has_value())
{
CHECK_RETURN(!is_java_generic_parameter(*retval));
return retval;
}
CHECK_RETURN(visited.empty());

const auto &entry =
generic_parameter_specialization_map.find(current_parameter)
->second.back();
current_parameter = to_java_generic_parameter(entry).get_name();
}
return {};
}

/// See get_recursively instantiated_type, the additional parameters just track
/// the recursion to prevent visiting the same depth again and specify which
/// stack depth is analyzed.
/// \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
/// \param visited: Tracks the visited parameter names
/// \param depth: Stack depth to analyze
/// \return if this type is not a generic type, it is returned as a valid
/// instantiation, if nothing can be found at the given depth, en empty
/// optional is returned
optionalt<pointer_typet>
select_pointer_typet::get_recursively_instantiated_type(
const irep_idt &parameter_name,
const generic_parameter_specialization_mapt
&generic_parameter_specialization_map,
generic_parameter_recursion_trackingt &visited,
const size_t depth) const
{
const auto &val = generic_parameter_specialization_map.find(parameter_name);
INVARIANT(
val != generic_parameter_specialization_map.end(),
"generic parameter must be a key in map");

const auto &replacements = val->second;

INVARIANT(
depth < replacements.size(), "cannot access elements outside stack");

// Check if there is a recursion loop, if yes return with nothing found
if(visited.find(parameter_name) != visited.end())
{
return {};
}

const size_t index = (replacements.size() - 1) - depth;
const auto &type = replacements[index];

if(!is_java_generic_parameter(type))
{
return type;
auto types_it = generic_parameter_specialization_map.find(parameter_name);
Copy link
Contributor

Choose a reason for hiding this comment

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

Commit message: note what the bug was and how this fixes it

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();
}

visited.insert(parameter_name);
const auto inst_val = get_recursively_instantiated_type(
to_java_generic_parameter(type).get_name(),
generic_parameter_specialization_map,
visited,
depth);
visited.erase(parameter_name);
return inst_val;
}

std::set<struct_tag_typet>
Expand Down
37 changes: 30 additions & 7 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 @@ -15,6 +15,7 @@ Author: Diffblue Ltd.

#include <vector>

#include "expr2java.h"
#include "java_types.h"
#include <util/optional.h>
#include <util/std_types.h>
Expand All @@ -23,18 +24,40 @@ 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
{
const generic_parameter_specialization_mapt &map;
const namespacet &ns;
};

template <typename ostream>
ostream &
operator<<(ostream &stm, const print_generic_parameter_specialization_map &map)
Copy link

Choose a reason for hiding this comment

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

👌 This is useful

{
stm << "Size: " << map.map.size() << "\n";
for(const auto &elt : map.map)
{
stm << elt.first << ": { ";
for(const auto &pointer_type : elt.second)
{
if(is_java_generic_parameter(pointer_type))
stm << to_java_generic_parameter(pointer_type).get_name() << "; ";
else
stm << type2java(pointer_type, map.ns) << "; ";
}
stm << "}\n";
}
return stm;
}

class namespacet;

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

public:
virtual ~select_pointer_typet() = default;
Expand Down