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 
20  &generic_parameter_specialization_map,
21  const namespacet &ns) const
22 {
23  (void)ns; // unused parameter
24  // if we have a map of generic parameters -> types and the pointer is
25  // a generic parameter, specialize it with concrete types
26  if(!generic_parameter_specialization_map.empty())
27  {
29  const auto &type = specialize_generics(
30  pointer_type, generic_parameter_specialization_map, visited);
31  INVARIANT(visited.empty(), "recursion stack must be empty here");
32  return type;
33  }
34  else
35  {
36  return pointer_type;
37  }
38 }
39 
43  &generic_parameter_specialization_map,
44  generic_parameter_recursion_trackingt &visited_nodes) const
45 {
47  {
48  const java_generic_parametert &parameter =
50  const irep_idt &parameter_name = parameter.get_name();
51 
52  // avoid infinite recursion by looking at each generic argument from
53  // previous assignments
54  if(visited_nodes.find(parameter_name) != visited_nodes.end())
55  {
57  parameter_name, generic_parameter_specialization_map);
58  return result.has_value() ? result.value() : pointer_type;
59  }
60 
61  if(generic_parameter_specialization_map.count(parameter_name) == 0)
62  {
63  // this means that the generic pointer_type has not been specialized
64  // in the current context (e.g., the method under test is generic);
65  // we return the pointer_type itself which is basically a pointer to
66  // its upper bound
67  return pointer_type;
68  }
69  const pointer_typet &type =
70  generic_parameter_specialization_map.find(parameter_name)->second.back();
71 
72  // generic parameters can be adopted from outer classes or superclasses so
73  // we may need to search for the concrete type recursively
74  if(!is_java_generic_parameter(type))
75  return type;
76 
77  visited_nodes.insert(parameter_name);
78  const auto returned_type = specialize_generics(
80  generic_parameter_specialization_map,
81  visited_nodes);
82  visited_nodes.erase(parameter_name);
83  return returned_type;
84  }
85  else if(pointer_type.subtype().id() == ID_struct_tag)
86  {
87  // if the pointer is an array, recursively specialize its element type
88  const auto &array_subtype = to_struct_tag_type(pointer_type.subtype());
89  if(is_java_array_tag(array_subtype.get_identifier()))
90  {
91  const typet &array_element_type = java_array_element_type(array_subtype);
92  if(array_element_type.id() == ID_pointer)
93  {
94  const pointer_typet &new_array_type = specialize_generics(
95  to_pointer_type(array_element_type),
96  generic_parameter_specialization_map,
97  visited_nodes);
98 
99  pointer_typet replacement_array_type = java_array_type('a');
100  replacement_array_type.subtype().set(ID_element_type, new_array_type);
101  return replacement_array_type;
102  }
103  }
104  }
105  return pointer_type;
106 }
107 
129  const irep_idt &parameter_name,
131  &generic_parameter_specialization_map) const
132 {
134  const size_t max_depth =
135  generic_parameter_specialization_map.find(parameter_name)->second.size();
136 
137  irep_idt current_parameter = parameter_name;
138  for(size_t depth = 0; depth < max_depth; depth++)
139  {
140  const auto retval = get_recursively_instantiated_type(
141  current_parameter, generic_parameter_specialization_map, visited, depth);
142  if(retval.has_value())
143  {
145  return retval;
146  }
147  CHECK_RETURN(visited.empty());
148 
149  const auto &entry =
150  generic_parameter_specialization_map.find(current_parameter)
151  ->second.back();
152  current_parameter = to_java_generic_parameter(entry).get_name();
153  }
154  return {};
155 }
156 
171  const irep_idt &parameter_name,
173  &generic_parameter_specialization_map,
175  const size_t depth) const
176 {
177  const auto &val = generic_parameter_specialization_map.find(parameter_name);
178  INVARIANT(
179  val != generic_parameter_specialization_map.end(),
180  "generic parameter must be a key in map");
181 
182  const auto &replacements = val->second;
183 
184  INVARIANT(
185  depth < replacements.size(), "cannot access elements outside stack");
186 
187  // Check if there is a recursion loop, if yes return with nothing found
188  if(visited.find(parameter_name) != visited.end())
189  {
190  return {};
191  }
192 
193  const size_t index = (replacements.size() - 1) - depth;
194  const auto &type = replacements[index];
195 
196  if(!is_java_generic_parameter(type))
197  {
198  return type;
199  }
200 
201  visited.insert(parameter_name);
202  const auto inst_val = get_recursively_instantiated_type(
203  to_java_generic_parameter(type).get_name(),
204  generic_parameter_specialization_map,
205  visited,
206  depth);
207  visited.erase(parameter_name);
208  return inst_val;
209 }
210 
211 std::set<struct_tag_typet>
213  const irep_idt &function_name,
214  const irep_idt &parameter_name,
215  const namespacet &) const
216 {
217  // unused parameters
218  (void)function_name;
219  (void)parameter_name;
220  return {};
221 }
The type of an expression, extends irept.
Definition: type.h:27
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:446
pointer_typet specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited_nodes) const
Specialize generic parameters in a pointer type based on the current map of parameters -> types.
const typet & java_array_element_type(const struct_tag_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:453
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
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:173
std::unordered_map< irep_idt, std::vector< reference_typet > > generic_parameter_specialization_mapt
const irep_idt & id() const
Definition: irep.h:259
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
nonstd::optional< T > optionalt
Definition: optional.h:35
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
Pre-defined types.
Class to hold a Java generic type parameter (also called type variable), e.g., T in List<T>.
Definition: java_types.h:397
const irep_idt get_name() const
Definition: java_types.h:424
virtual std::set< struct_tag_typet > get_parameter_alternative_types(const irep_idt &function_name, const irep_idt &parameter_name, const namespacet &ns) const
Get alternative types for a method parameter, e.g., based on the casts in the function body.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
const typet & subtype() const
Definition: type.h:38
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:284
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286