replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #4897 from diffblue/cleanup/generic_parameter_specialization_map_keys 

Cleanup generic_parameter_specialization_map_keys
This commit is contained in:
Nathan Phillips 2019-07-16 14:24:57 +01:00 committed by GitHub
parent da8a63ef93 508a717c0d
commit c6c0eff1bc
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
4 changed files with 78 additions and 84 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

137
jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp
View File

@ -2,7 +2,7 @@
#include "generic_parameter_specialization_map_keys.h"
#include <iterator>
#include <util/range.h>
/// \param type: Source type
/// \return The vector of implicitly generic and (explicitly) generic type
@ -44,26 +44,12 @@ void generic_parameter_specialization_map_keyst::insert_pairs(
const std::vector<reference_typet> &types)
{
INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
PRECONDITION(parameters.size() == types.size());
// Pair up the parameters and types for easier manipulation later
std::vector<std::pair<java_generic_parametert, reference_typet>> pairs;
pairs.reserve(parameters.size());
std::transform(
parameters.begin(),
parameters.end(),
types.begin(),
std::back_inserter(pairs),
[&](java_generic_parametert param, reference_typet type)
{
return std::make_pair(param, type);
});
for(const auto &pair : pairs)
for(const auto &pair : make_range(parameters).zip(types))
{
// Only add the pair if the type is not the parameter itself, e.g.,
// pair.first = pair.second = java::A::T. This can happen for example
// when initiating a pointer to an implicitly java generic class type
// when initializing a pointer to an implicitly generic Java class type
// in gen_nondet_init and would result in a loop when the map is used
// to look up the type of the parameter.
if(
@ -72,13 +58,13 @@ void generic_parameter_specialization_map_keyst::insert_pairs(
pair.first.get_name()))
{
const irep_idt &key = pair.first.get_name();
if(generic_parameter_specialization_map.count(key) == 0)
generic_parameter_specialization_map.emplace(
key, std::vector<reference_typet>());
(*generic_parameter_specialization_map.find(key))
.second.push_back(pair.second);
const auto map_it = generic_parameter_specialization_map
.emplace(key, std::vector<reference_typet>{})
.first;
map_it->second.push_back(pair.second);
// We added something, so pop it when this is destroyed:
// We added something; pop it when this
// generic_parameter_specialization_map_keyst is destroyed
erase_keys.push_back(key);
}
}
@ -94,40 +80,42 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer(
const pointer_typet &pointer_type,
const typet &pointer_subtype_struct)
{
if(is_java_generic_type(pointer_type))
if(!is_java_generic_type(pointer_type))
return;
// The supplied type must be the full type of the pointer's subtype
PRECONDITION(
pointer_type.subtype().get(ID_identifier) ==
pointer_subtype_struct.get(ID_name));
// If the pointer points to:
// - an incomplete class or
// - a class that is neither generic nor implicitly generic (this
// may be due to unsupported class signature)
// then ignore the generic types in the pointer and do not add any pairs.
// TODO TG-1996 should decide how mocking and generics should work
// together. Currently an incomplete class is never marked as generic. If
// this changes in TG-1996 then the condition below should be updated.
if(to_java_class_type(pointer_subtype_struct).get_is_stub())
return;
if(
!is_java_generic_class_type(pointer_subtype_struct) &&
!is_java_implicitly_generic_class_type(pointer_subtype_struct))
{
// The supplied type must be the full type of the pointer's subtype
PRECONDITION(
pointer_type.subtype().get(ID_identifier) ==
pointer_subtype_struct.get(ID_name));
// If the pointer points to:
// - an incomplete class or
// - a class that is neither generic nor implicitly generic (this
// may be due to unsupported class signature)
// then ignore the generic types in the pointer and do not add any pairs.
// TODO TG-1996 should decide how mocking and generics should work
// together. Currently an incomplete class is never marked as generic. If
// this changes in TG-1996 then the condition below should be updated.
if(
!to_java_class_type(pointer_subtype_struct).get_is_stub() &&
(is_java_generic_class_type(pointer_subtype_struct) ||
is_java_implicitly_generic_class_type(pointer_subtype_struct)))
{
const java_generic_typet &generic_pointer =
to_java_generic_type(pointer_type);
const std::vector<java_generic_parametert> &generic_parameters =
get_all_generic_parameters(pointer_subtype_struct);
INVARIANT(
generic_pointer.generic_type_arguments().size() ==
generic_parameters.size(),
"All generic parameters of the pointer type need to be specified");
insert_pairs(
generic_parameters, generic_pointer.generic_type_arguments());
}
return;
}
const java_generic_typet &generic_pointer =
to_java_generic_type(pointer_type);
const std::vector<java_generic_parametert> &generic_parameters =
get_all_generic_parameters(pointer_subtype_struct);
const java_generic_typet::generic_type_argumentst &type_args =
generic_pointer.generic_type_arguments();
INVARIANT(
type_args.size() == generic_parameters.size(),
"All generic parameters of the pointer type need to be specified");
insert_pairs(generic_parameters, type_args);
}
/// Add a pair of a parameter and its types for each generic parameter of the
@ -151,24 +139,29 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol(
// then ignore the generic types in the struct_tag_type and do not add any
// pairs.
// TODO TG-1996 should decide how mocking and generics should work
// together. Currently an incomplete class is never marked as generic. If
// this changes in TG-1996 then the condition below should be updated.
// together. Currently an incomplete class is never marked as generic. If
// this changes in TG-1996 then the condition below should be updated.
if(!is_java_generic_struct_tag_type(struct_tag_type))
return;
if(to_java_class_type(symbol_struct).get_is_stub())
return;
if(
is_java_generic_struct_tag_type(struct_tag_type) &&
!to_java_class_type(symbol_struct).get_is_stub() &&
(is_java_generic_class_type(symbol_struct) ||
is_java_implicitly_generic_class_type(symbol_struct)))
!is_java_generic_class_type(symbol_struct) &&
!is_java_implicitly_generic_class_type(symbol_struct))
{
const java_generic_struct_tag_typet &generic_symbol =
to_java_generic_struct_tag_type(struct_tag_type);
const std::vector<java_generic_parametert> &generic_parameters =
get_all_generic_parameters(symbol_struct);
INVARIANT(
generic_symbol.generic_types().size() == generic_parameters.size(),
"All generic parameters of the superclass need to be concretized");
insert_pairs(generic_parameters, generic_symbol.generic_types());
return;
}
const java_generic_struct_tag_typet &generic_symbol =
to_java_generic_struct_tag_type(struct_tag_type);
const std::vector<java_generic_parametert> &generic_parameters =
get_all_generic_parameters(symbol_struct);
const java_generic_typet::generic_type_argumentst &type_args =
generic_symbol.generic_types();
INVARIANT(
type_args.size() == generic_parameters.size(),
"All generic parameters of the superclass need to be concretized");
insert_pairs(generic_parameters, type_args);
}

7
jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h
View File

@ -33,11 +33,12 @@ public:
{
for(const auto key : erase_keys)
{
PRECONDITION(generic_parameter_specialization_map.count(key) != 0);
auto &val = generic_parameter_specialization_map.find(key)->second;
const auto map_it = generic_parameter_specialization_map.find(key);
PRECONDITION(map_it != generic_parameter_specialization_map.end());
std::vector<reference_typet> &val = map_it->second;
val.pop_back();
if(val.empty())
generic_parameter_specialization_map.erase(key);
generic_parameter_specialization_map.erase(map_it);
}
}

4
jbmc/src/java_bytecode/java_object_factory.cpp
View File

@ -487,8 +487,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
// If we are changing the pointer, we generate code for creating a pointer
// to the substituted type instead
// TODO if we are comparing array types we need to compare their element
// types. this is for now done by implementing equality function especially
// for java types, technical debt TG-2707
// types. this is for now done by implementing equality function especially
// for java types, technical debt TG-2707
if(!equal_java_types(replacement_pointer_type, pointer_type))
{
// update generic_parameter_specialization_map for the new pointer

14
jbmc/src/java_bytecode/select_pointer_type.cpp
View File

@ -18,9 +18,8 @@ pointer_typet select_pointer_typet::convert_pointer_type(
const pointer_typet &pointer_type,
const generic_parameter_specialization_mapt
&generic_parameter_specialization_map,
const namespacet &ns) const
const namespacet &) const
{
(void)ns; // unused parameter
// if we have a map of generic parameters -> types and the pointer is
// a generic parameter, specialize it with concrete types
if(!generic_parameter_specialization_map.empty())
@ -51,14 +50,16 @@ pointer_typet select_pointer_typet::specialize_generics(
// avoid infinite recursion by looking at each generic argument from
// previous assignments
if(visited_nodes.find(parameter_name) != visited_nodes.end())
if(visited_nodes.count(parameter_name) != 0)
{
const optionalt<pointer_typet> result = get_recursively_instantiated_type(
parameter_name, generic_parameter_specialization_map);
return result.has_value() ? result.value() : pointer_type;
}
if(generic_parameter_specialization_map.count(parameter_name) == 0)
const auto specialization =
generic_parameter_specialization_map.find(parameter_name);
if(specialization == generic_parameter_specialization_map.end())
{
// this means that the generic pointer_type has not been specialized
// in the current context (e.g., the method under test is generic);
@ -66,8 +67,7 @@ pointer_typet select_pointer_typet::specialize_generics(
// its upper bound
return pointer_type;
}
const pointer_typet &type =
generic_parameter_specialization_map.find(parameter_name)->second.back();
const pointer_typet &type = specialization->second.back();
// generic parameters can be adopted from outer classes or superclasses so
// we may need to search for the concrete type recursively
@ -111,7 +111,7 @@ pointer_typet select_pointer_typet::specialize_generics(
///
/// Example:
/// `class MyGeneric<T,U> { MyGeneric<U,T> gen; T t;}`
/// When instantiating `MyGeneric<Integer,String> my` we need to for example
/// For example, when instantiating `MyGeneric<Integer,String> my` we need to
/// resolve the type of `my.gen.t`. The map would in this context contain
/// - T -> (Integer, U)
/// - U -> (String, T)