CBMC
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 
16 #include "java_types.h"
17 
18 #include <util/std_types.h>
19 
23  &generic_parameter_specialization_map,
24  const namespacet &) const
25 {
26  return specialize_generics(
27  pointer_type, generic_parameter_specialization_map);
28 }
29 
33  &generic_parameter_specialization_map) const
34 {
35  auto parameter = type_try_dynamic_cast<java_generic_parametert>(pointer_type);
36  if(parameter != nullptr)
37  {
38  irep_idt parameter_name = parameter->get_name();
39 
40  // Make a local copy of the specialization map to unwind
42  generic_parameter_specialization_map;
43  while(true)
44  {
45  const std::optional<reference_typet> specialization =
46  spec_map_copy.pop(parameter_name);
47  if(!specialization)
48  {
49  // This means that the generic pointer_type has not been specialized
50  // in the current context (e.g., the method under test is generic);
51  // we return the pointer_type itself which is a pointer to its upper
52  // bound
53  return pointer_type;
54  }
55 
56  if(!is_java_generic_parameter(*specialization))
57  return *specialization;
58  parameter_name = to_java_generic_parameter(*specialization).get_name();
59  }
60  }
61 
62  auto base_type =
63  type_try_dynamic_cast<struct_tag_typet>(pointer_type.base_type());
64  if(base_type != nullptr && is_java_array_tag(base_type->get_identifier()))
65  {
66  // if the pointer is an array, recursively specialize its element type
67  const auto *array_element_type =
68  type_try_dynamic_cast<pointer_typet>(java_array_element_type(*base_type));
69  if(array_element_type == nullptr)
70  return pointer_type;
71 
72  const pointer_typet &new_array_type = specialize_generics(
73  *array_element_type, generic_parameter_specialization_map);
74 
75  pointer_typet replacement_array_type = java_array_type('a');
76  replacement_array_type.base_type().set(ID_element_type, new_array_type);
77  return replacement_array_type;
78  }
79 
80  return pointer_type;
81 }
82 
83 std::set<struct_tag_typet>
85  const irep_idt &,
86  const irep_idt &,
87  const namespacet &) const
88 {
89  return {};
90 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
void pop(std::size_t container_index)
Pop the top of the specialization stack for a given container.
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
const irep_idt get_name() const
Definition: java_types.h:798
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
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.
pointer_typet specialize_generics(const pointer_typet &pointer_type, const generic_parameter_specialization_mapt &generic_parameter_specialization_map) const
Specialize generic parameters in a pointer type based on the current map of parameters -> types.
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 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:144
java_reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:109
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:233
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:819
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:826
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
Pre-defined types.