cprover
select_pointer_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3  Module: Java Bytecode Language Conversion
4 
5  Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
12 
13 #include "select_pointer_type.h"
14 #include "java_types.h"
15 #include <util/std_types.h>
16 
29  &generic_parameter_specialization_map,
30  const namespacet &ns) const
31 {
32  // if we have a map of generic parameters -> types and the pointer is
33  // a generic parameter, specialize it with concrete types
34  if(!generic_parameter_specialization_map.empty())
35  {
37  const auto &type = specialize_generics(
38  pointer_type, generic_parameter_specialization_map, visited);
39  INVARIANT(visited.empty(), "recursion stack must be empty here");
40  return type;
41  }
42  else
43  {
44  return pointer_type;
45  }
46 }
47 
69  &generic_parameter_specialization_map,
70  generic_parameter_recursion_trackingt &visited_nodes) const
71 {
73  {
74  const java_generic_parametert &parameter =
76  const irep_idt &parameter_name = parameter.get_name();
77 
78  // avoid infinite recursion by looking at each generic argument from
79  // previous assignments
80  if(visited_nodes.find(parameter_name) != visited_nodes.end())
81  {
83  parameter_name, generic_parameter_specialization_map);
84  return result.has_value() ? result.value() : pointer_type;
85  }
86 
87  if(generic_parameter_specialization_map.count(parameter_name) == 0)
88  {
89  // this means that the generic pointer_type has not been specialized
90  // in the current context (e.g., the method under test is generic);
91  // we return the pointer_type itself which is basically a pointer to
92  // its upper bound
93  return pointer_type;
94  }
95  const pointer_typet &type =
96  generic_parameter_specialization_map.find(parameter_name)->second.back();
97 
98  // generic parameters can be adopted from outer classes or superclasses so
99  // we may need to search for the concrete type recursively
100  if(!is_java_generic_parameter(type))
101  return type;
102 
103  visited_nodes.insert(parameter_name);
104  const auto returned_type = specialize_generics(
106  generic_parameter_specialization_map,
107  visited_nodes);
108  visited_nodes.erase(parameter_name);
109  return returned_type;
110  }
111  else if(pointer_type.subtype().id() == ID_symbol)
112  {
113  // if the pointer is an array, recursively specialize its element type
114  const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());
115  if(is_java_array_tag(array_subtype.get_identifier()))
116  {
117  const typet &array_element_type = java_array_element_type(array_subtype);
118  if(array_element_type.id() == ID_pointer)
119  {
120  const pointer_typet &new_array_type = specialize_generics(
121  to_pointer_type(array_element_type),
122  generic_parameter_specialization_map,
123  visited_nodes);
124 
125  pointer_typet replacement_array_type = java_array_type('a');
126  replacement_array_type.subtype().set(ID_element_type, new_array_type);
127  return replacement_array_type;
128  }
129  }
130  }
131  return pointer_type;
132 }
133 
145  const irep_idt &parameter_name,
147  &generic_parameter_specialization_map) const
148 {
150  const size_t max_depth =
151  generic_parameter_specialization_map.find(parameter_name)->second.size();
152 
153  irep_idt current_parameter = parameter_name;
154  for(size_t depth = 0; depth < max_depth; depth++)
155  {
156  const auto retval = get_recursively_instantiated_type(
157  current_parameter, generic_parameter_specialization_map, visited, depth);
158  if(retval.has_value())
159  {
161  return retval;
162  }
163  CHECK_RETURN(visited.empty());
164 
165  const auto &entry =
166  generic_parameter_specialization_map.find(current_parameter)
167  ->second.back();
168  current_parameter = to_java_generic_parameter(entry).get_name();
169  }
170  return {};
171 }
172 
187  const irep_idt &parameter_name,
189  &generic_parameter_specialization_map,
191  const size_t depth) const
192 {
193  const auto &val = generic_parameter_specialization_map.find(parameter_name);
194  INVARIANT(
195  val != generic_parameter_specialization_map.end(),
196  "generic parameter must be a key in map");
197 
198  const auto &replacements = val->second;
199 
200  INVARIANT(
201  depth < replacements.size(), "cannot access elements outside stack");
202 
203  // Check if there is a recursion loop, if yes return with nothing found
204  if(visited.find(parameter_name) != visited.end())
205  {
206  return {};
207  }
208 
209  const size_t index = (replacements.size() - 1) - depth;
210  const auto &type = replacements[index];
211 
212  if(!is_java_generic_parameter(type))
213  {
214  return type;
215  }
216 
217  visited.insert(parameter_name);
218  const auto inst_val = get_recursively_instantiated_type(
219  to_java_generic_parameter(type).get_name(),
220  generic_parameter_specialization_map,
221  visited,
222  depth);
223  visited.erase(parameter_name);
224  return inst_val;
225 }
The type of an expression.
Definition: type.h:22
std::set< irep_idt > generic_parameter_recursion_trackingt
optionalt< pointer_typet > get_recursively_instantiated_type(const irep_idt &, const generic_parameter_specialization_mapt &, generic_parameter_recursion_trackingt &, const size_t) const
See get_recursively instantiated_type, the additional parameters just track the recursion to prevent ...
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
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 symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
const typet & java_array_element_type(const symbol_typet &array_symbol)
Return a const reference to the element type of a given java array type.
Definition: java_types.cpp:129
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:399
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:94
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:174
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const irep_idt & id() const
Definition: irep.h:259
A reference into the symbol table.
Definition: std_types.h:110
The pointer type.
Definition: std_types.h:1435
nonstd::optional< T > optionalt
Definition: optional.h:35
TO_BE_DOCUMENTED.
Definition: namespace.h:74
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
pointer_typet specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited) const
Specialize generic parameters in a pointer type based on the current map of parameters -> types...
API to type classes.
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
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1459
const typet & subtype() const
Definition: type.h:33
virtual pointer_typet convert_pointer_type(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, const namespacet &ns) const
Select what type should be used for a given pointer type.
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
const irep_idt & get_identifier() const
Definition: std_types.h:123
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286