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 &) const
22 {
23  return specialize_generics(
24  pointer_type, generic_parameter_specialization_map);
25 }
26 
30  &generic_parameter_specialization_map) const
31 {
32  auto parameter = type_try_dynamic_cast<java_generic_parametert>(pointer_type);
33  if(parameter != nullptr)
34  {
35  irep_idt parameter_name = parameter->get_name();
36 
37  // Make a local copy of the specialization map to unwind
39  generic_parameter_specialization_map;
40  while(true)
41  {
42  const optionalt<reference_typet> specialization =
43  spec_map_copy.pop(parameter_name);
44  if(!specialization)
45  {
46  // This means that the generic pointer_type has not been specialized
47  // in the current context (e.g., the method under test is generic);
48  // we return the pointer_type itself which is a pointer to its upper
49  // bound
50  return pointer_type;
51  }
52 
53  if(!is_java_generic_parameter(*specialization))
54  return *specialization;
55  parameter_name = to_java_generic_parameter(*specialization).get_name();
56  }
57  }
58 
59  auto subtype =
60  type_try_dynamic_cast<struct_tag_typet>(pointer_type.subtype());
61  if(subtype != nullptr && is_java_array_tag(subtype->get_identifier()))
62  {
63  // if the pointer is an array, recursively specialize its element type
64  const auto *array_element_type =
65  type_try_dynamic_cast<pointer_typet>(java_array_element_type(*subtype));
66  if(array_element_type == nullptr)
67  return pointer_type;
68 
69  const pointer_typet &new_array_type = specialize_generics(
70  *array_element_type, generic_parameter_specialization_map);
71 
72  pointer_typet replacement_array_type = java_array_type('a');
73  replacement_array_type.subtype().set(ID_element_type, new_array_type);
74  return replacement_array_type;
75  }
76 
77  return pointer_type;
78 }
79 
80 std::set<struct_tag_typet>
82  const irep_idt &,
83  const irep_idt &,
84  const namespacet &) const
85 {
86  return {};
87 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
select_pointer_type.h
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
java_array_element_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:145
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:232
select_pointer_typet::get_parameter_alternative_types
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.
Definition: select_pointer_type.cpp:81
generic_parameter_specialization_mapt
Author: Diffblue Ltd.
Definition: generic_parameter_specialization_map.h:24
select_pointer_typet::convert_pointer_type
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.
Definition: select_pointer_type.cpp:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
java_generic_parametert::get_name
const irep_idt get_name() const
Definition: java_types.h:801
is_java_generic_parameter
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:821
std_types.h
Pre-defined types.
java_array_type
java_reference_typet java_array_type(const char subtype)
Construct an array pointer type.
Definition: java_types.cpp:110
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
to_java_generic_parameter
const java_generic_parametert & to_java_generic_parameter(const typet &type)
Definition: java_types.h:828
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
select_pointer_typet::specialize_generics
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.
Definition: select_pointer_type.cpp:27
java_types.h
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
generic_parameter_specialization_mapt::pop
void pop(std::size_t container_index)
Pop the top of the specialization stack for a given container.
Definition: generic_parameter_specialization_map.cpp:49