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 
28  &generic_parameter_specialization_map,
29  const namespacet &ns) const
30 {
31  // if we have a map of generic parameters -> types and the pointer is
32  // a generic parameter, specialize it with concrete types
33  if(!generic_parameter_specialization_map.empty())
34  {
36  const auto &type = specialize_generics(
37  pointer_type, generic_parameter_specialization_map, visited);
38  INVARIANT(visited.empty(), "recursion stack must be empty here");
39  return type;
40  }
41  else
42  {
43  return pointer_type;
44  }
45 }
46 
68  &generic_parameter_specialization_map,
69  generic_parameter_recursion_trackingt &visited_nodes) const
70 {
72  {
73  const java_generic_parametert &parameter =
75  const irep_idt &parameter_name = parameter.get_name();
76 
77  // avoid infinite recursion by looking at each generic argument from
78  // previous assignments
79  if(visited_nodes.find(parameter_name) != visited_nodes.end())
80  {
82  parameter_name, generic_parameter_specialization_map);
83  return result.has_value() ? result.value() : pointer_type;
84  }
85 
86  if(generic_parameter_specialization_map.count(parameter_name) == 0)
87  {
88  // this means that the generic pointer_type has not been specialized
89  // in the current context (e.g., the method under test is generic);
90  // we return the pointer_type itself which is basically a pointer to
91  // its upper bound
92  return pointer_type;
93  }
94  const pointer_typet &type =
95  generic_parameter_specialization_map.find(parameter_name)->second.back();
96 
97  // generic parameters can be adopted from outer classes or superclasses so
98  // we may need to search for the concrete type recursively
99  if(!is_java_generic_parameter(type))
100  return type;
101 
102  visited_nodes.insert(parameter_name);
103  const auto returned_type = specialize_generics(
105  generic_parameter_specialization_map,
106  visited_nodes);
107  visited_nodes.erase(parameter_name);
108  return returned_type;
109  }
110  else if(pointer_type.subtype().id() == ID_symbol)
111  {
112  // if the pointer is an array, recursively specialize its element type
113  const symbol_typet &array_subtype = to_symbol_type(pointer_type.subtype());
114  if(is_java_array_tag(array_subtype.get_identifier()))
115  {
116  const typet &array_element_type = java_array_element_type(array_subtype);
117  if(array_element_type.id() == ID_pointer)
118  {
119  const pointer_typet &new_array_type = specialize_generics(
120  to_pointer_type(array_element_type),
121  generic_parameter_specialization_map,
122  visited_nodes);
123 
124  pointer_typet replacement_array_type = java_array_type('a');
125  replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
126  return replacement_array_type;
127  }
128  }
129  }
130  return pointer_type;
131 }
132 
144  const irep_idt &parameter_name,
146  &generic_parameter_specialization_map) const
147 {
149  const size_t max_depth =
150  generic_parameter_specialization_map.find(parameter_name)->second.size();
151 
152  irep_idt current_parameter = parameter_name;
153  for(size_t depth = 0; depth < max_depth; depth++)
154  {
155  const auto retval = get_recursively_instantiated_type(
156  current_parameter, generic_parameter_specialization_map, visited, depth);
157  if(retval.has_value())
158  {
160  return retval;
161  }
162  CHECK_RETURN(visited.empty());
163 
164  const auto &entry =
165  generic_parameter_specialization_map.find(current_parameter)
166  ->second.back();
167  current_parameter = to_java_generic_parameter(entry).get_name();
168  }
169  return {};
170 }
171 
186  const irep_idt &parameter_name,
188  &generic_parameter_specialization_map,
190  const size_t depth) const
191 {
192  const auto &val = generic_parameter_specialization_map.find(parameter_name);
193  INVARIANT(
194  val != generic_parameter_specialization_map.end(),
195  "generic parameter must be a key in map");
196 
197  const auto &replacements = val->second;
198 
199  INVARIANT(
200  depth < replacements.size(), "cannot access elements outside stack");
201 
202  // Check if there is a recursion loop, if yes return with nothing found
203  if(visited.find(parameter_name) != visited.end())
204  {
205  return {};
206  }
207 
208  const size_t index = (replacements.size() - 1) - depth;
209  const auto &type = replacements[index];
210 
211  if(!is_java_generic_parameter(type))
212  {
213  return type;
214  }
215 
216  visited.insert(parameter_name);
217  const auto inst_val = get_recursively_instantiated_type(
218  to_java_generic_parameter(type).get_name(),
219  generic_parameter_specialization_map,
220  visited,
221  depth);
222  visited.erase(parameter_name);
223  return inst_val;
224 }
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:281
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:288
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
reference_typet java_array_type(const char subtype)
Definition: java_types.cpp:90
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:137
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
const irep_idt & id() const
Definition: irep.h:189
A reference into the symbol table.
Definition: std_types.h:110
The pointer type.
Definition: std_types.h:1426
nonstd::optional< T > optionalt
Definition: optional.h:35
TO_BE_DOCUMENTED.
Definition: namespace.h:74
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:232
const irep_idt get_name() const
Definition: java_types.h:259
typet java_array_element_type(const symbol_typet &array_type)
Return the type of the elements of a given java array type.
Definition: java_types.cpp:126
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Definition: std_types.h:1450
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:214