cprover
generic_parameter_specialization_map_keys.cpp
Go to the documentation of this file.
1 
4 
5 #include <iterator>
6 
10 const std::vector<java_generic_parametert>
12 {
16  std::vector<java_generic_parametert> generic_parameters;
18  {
19  const java_implicitly_generic_class_typet &implicitly_generic_class =
21  generic_parameters.insert(
22  generic_parameters.end(),
23  implicitly_generic_class.implicit_generic_types().begin(),
24  implicitly_generic_class.implicit_generic_types().end());
25  }
27  {
28  const java_generic_class_typet &generic_class =
30  generic_parameters.insert(
31  generic_parameters.end(),
32  generic_class.generic_types().begin(),
33  generic_class.generic_types().end());
34  }
35  return generic_parameters;
36 }
37 
43  const std::vector<java_generic_parametert> &parameters,
44  const std::vector<reference_typet> &types)
45 {
46  INVARIANT(erase_keys.empty(), "insert_pairs should only be called once");
47  PRECONDITION(parameters.size() == types.size());
48 
49  // Pair up the parameters and types for easier manipulation later
50  std::vector<std::pair<java_generic_parametert, reference_typet>> pairs;
51  pairs.reserve(parameters.size());
52  std::transform(
53  parameters.begin(),
54  parameters.end(),
55  types.begin(),
56  std::back_inserter(pairs),
58  {
59  return std::make_pair(param, type);
60  });
61 
62  for(const auto &pair : pairs)
63  {
64  // Only add the pair if the type is not the parameter itself, e.g.,
65  // pair.first = pair.second = java::A::T. This can happen for example
66  // when initiating a pointer to an implicitly java generic class type
67  // in gen_nondet_init and would result in a loop when the map is used
68  // to look up the type of the parameter.
69  if(
70  !(is_java_generic_parameter(pair.second) &&
71  to_java_generic_parameter(pair.second).get_name() ==
72  pair.first.get_name()))
73  {
74  const irep_idt &key = pair.first.get_name();
75  if(generic_parameter_specialization_map.count(key) == 0)
77  key, std::vector<reference_typet>());
79  .second.push_back(pair.second);
80 
81  // We added something, so pop it when this is destroyed:
82  erase_keys.push_back(key);
83  }
84  }
85 }
86 
95  const typet &pointer_subtype_struct)
96 {
98  {
99  // The supplied type must be the full type of the pointer's subtype
100  PRECONDITION(
101  pointer_type.subtype().get(ID_identifier) ==
102  pointer_subtype_struct.get(ID_name));
103 
104  // If the pointer points to:
105  // - an incomplete class or
106  // - a class that is neither generic nor implicitly generic (this
107  // may be due to unsupported class signature)
108  // then ignore the generic types in the pointer and do not add any pairs.
109  // TODO TG-1996 should decide how mocking and generics should work
110  // together. Currently an incomplete class is never marked as generic. If
111  // this changes in TG-1996 then the condition below should be updated.
112  if(
113  !to_java_class_type(pointer_subtype_struct).get_is_stub() &&
114  (is_java_generic_class_type(pointer_subtype_struct) ||
115  is_java_implicitly_generic_class_type(pointer_subtype_struct)))
116  {
117  const java_generic_typet &generic_pointer =
119  const std::vector<java_generic_parametert> &generic_parameters =
120  get_all_generic_parameters(pointer_subtype_struct);
121 
122  INVARIANT(
123  generic_pointer.generic_type_arguments().size() ==
124  generic_parameters.size(),
125  "All generic parameters of the pointer type need to be specified");
126 
127  insert_pairs(
128  generic_parameters, generic_pointer.generic_type_arguments());
129  }
130  }
131 }
132 
143  const struct_tag_typet &struct_tag_type,
144  const typet &symbol_struct)
145 {
146  // If the struct is:
147  // - an incomplete class or
148  // - a class that is neither generic nor implicitly generic (this
149  // may be due to unsupported class signature)
150  // then ignore the generic types in the struct_tag_type and do not add any
151  // pairs.
152  // TODO TG-1996 should decide how mocking and generics should work
153  // together. Currently an incomplete class is never marked as generic. If
154  // this changes in TG-1996 then the condition below should be updated.
155  if(
156  is_java_generic_struct_tag_type(struct_tag_type) &&
157  !to_java_class_type(symbol_struct).get_is_stub() &&
158  (is_java_generic_class_type(symbol_struct) ||
160  {
161  const java_generic_struct_tag_typet &generic_symbol =
162  to_java_generic_struct_tag_type(struct_tag_type);
163 
164  const std::vector<java_generic_parametert> &generic_parameters =
165  get_all_generic_parameters(symbol_struct);
166 
167  INVARIANT(
168  generic_symbol.generic_types().size() == generic_parameters.size(),
169  "All generic parameters of the superclass need to be concretized");
170 
171  insert_pairs(generic_parameters, generic_symbol.generic_types());
172  }
173 }
is_java_generic_class_type
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:565
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
java_generic_typet
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:483
reference_typet
The reference type.
Definition: std_types.h:1565
java_implicitly_generic_class_typet::implicit_generic_types
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:654
typet
The type of an expression, extends irept.
Definition: type.h:27
generic_parameter_specialization_map_keys.h
Author: Diffblue Ltd.
java_generic_parametert
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition: java_types.h:397
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
is_java_implicitly_generic_class_type
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:670
to_java_generic_class_type
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:573
java_generic_struct_tag_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:764
java_generic_class_typet::generic_types
const generic_typest & generic_types() const
Definition: java_types.h:552
java_generic_parametert::get_name
const irep_idt get_name() const
Definition: java_types.h:424
generic_parameter_specialization_map_keyst::erase_keys
std::vector< irep_idt > erase_keys
Keys of the entries to pop on destruction.
Definition: generic_parameter_specialization_map_keys.h:61
to_java_generic_struct_tag_type
const java_generic_struct_tag_typet & to_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:788
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:495
is_java_generic_parameter
bool is_java_generic_parameter(const typet &type)
Checks whether the type is a java generic parameter/variable, e.g., T in List<T>.
Definition: java_types.h:446
is_java_generic_struct_tag_type
bool is_java_generic_struct_tag_type(const typet &type)
Definition: java_types.h:780
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:517
java_implicitly_generic_class_typet
Type to hold a Java class that is implicitly generic, e.g., an inner class of a generic outer class o...
Definition: java_types.h:637
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
generic_parameter_specialization_map_keyst::generic_parameter_specialization_map
generic_parameter_specialization_mapt & generic_parameter_specialization_map
Generic parameter specialization map to modify.
Definition: generic_parameter_specialization_map_keys.h:59
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:524
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:453
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
to_java_implicitly_generic_class_type
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:678
get_all_generic_parameters
const std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
Author: Diffblue Ltd.
Definition: generic_parameter_specialization_map_keys.cpp:11
generic_parameter_specialization_map_keyst::insert_pairs_for_symbol
void insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type t...
Definition: generic_parameter_specialization_map_keys.cpp:142
java_generic_struct_tag_typet
Type for a generic symbol, extends struct_tag_typet with a vector of java generic types.
Definition: java_types.h:754
java_generic_class_typet
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:542
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246
java_class_typet::get_is_stub
bool get_is_stub() const
Definition: java_types.h:179
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
validation_modet::INVARIANT
generic_parameter_specialization_map_keyst::insert_pairs
void insert_pairs(const std::vector< java_generic_parametert > &parameters, const std::vector< reference_typet > &types)
Add pairs to the controlled map.
Definition: generic_parameter_specialization_map_keys.cpp:42
generic_parameter_specialization_map_keyst::insert_pairs_for_pointer
void insert_pairs_for_pointer(const pointer_typet &pointer_type, const typet &pointer_subtype_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic pointer type ...
Definition: generic_parameter_specialization_map_keys.cpp:93