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  !pointer_subtype_struct.get_bool(ID_incomplete_class) &&
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 symbol_typet &symbol_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 symbol_type and do not add any pairs.
151  // TODO TG-1996 should decide how mocking and generics should work
152  // together. Currently an incomplete class is never marked as generic. If
153  // this changes in TG-1996 then the condition below should be updated.
154  if(
155  is_java_generic_symbol_type(symbol_type) &&
156  !symbol_struct.get_bool(ID_incomplete_class) &&
157  (is_java_generic_class_type(symbol_struct) ||
159  {
160  const java_generic_symbol_typet &generic_symbol =
161  to_java_generic_symbol_type(symbol_type);
162 
163  const std::vector<java_generic_parametert> &generic_parameters =
164  get_all_generic_parameters(symbol_struct);
165 
166  INVARIANT(
167  generic_symbol.generic_types().size() == generic_parameters.size(),
168  "All generic parameters of the superclass need to be concretized");
169 
170  insert_pairs(generic_parameters, generic_symbol.generic_types());
171  }
172 }
The type of an expression.
Definition: type.h:22
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
bool is_java_generic_symbol_type(const typet &type)
Definition: java_types.h:724
const java_generic_class_typet & to_java_generic_class_type(const java_class_typet &type)
Definition: java_types.h:517
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:392
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:399
std::vector< irep_idt > erase_keys
Keys of the entries to pop on destruction.
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:441
const java_generic_symbol_typet & to_java_generic_symbol_type(const typet &type)
Definition: java_types.h:732
Class to hold a class with generics, extends the java class type with a vector of java generic type p...
Definition: java_types.h:486
A reference into the symbol table.
Definition: std_types.h:110
The pointer type.
Definition: std_types.h:1435
const java_implicitly_generic_class_typet & to_java_implicitly_generic_class_type(const java_class_typet &type)
Definition: java_types.h:622
const std::vector< java_generic_parametert > get_all_generic_parameters(const typet &type)
Author: Diffblue Ltd.
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const generic_typest & generic_types() const
Definition: java_types.h:708
bool is_java_generic_class_type(const typet &type)
Definition: java_types.h:509
Type for a generic symbol, extends symbol_typet with a vector of java generic types.
Definition: java_types.h:698
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const implicit_generic_typest & implicit_generic_types() const
Definition: java_types.h:598
The reference type.
Definition: std_types.h:1492
Class to hold type with generic type arguments, for example java.util.List in either a reference of t...
Definition: java_types.h:429
const 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 ...
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:464
const void insert_pairs(const std::vector< java_generic_parametert > &parameters, const std::vector< reference_typet > &types)
Add pairs to the controlled map.
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>...
Definition: java_types.h:343
const irep_idt get_name() const
Definition: java_types.h:370
bool is_java_generic_type(const typet &type)
Definition: java_types.h:457
const typet & subtype() const
Definition: type.h:33
bool is_java_implicitly_generic_class_type(const typet &type)
Definition: java_types.h:614
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:581
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:227
const generic_typest & generic_types() const
Definition: java_types.h:496
const void insert_pairs_for_symbol(const symbol_typet &symbol_type, const typet &symbol_struct)
Add a pair of a parameter and its types for each generic parameter of the given generic symbol type t...
generic_parameter_specialization_mapt & generic_parameter_specialization_map
Generic parameter specialization map to modify.