cprover
ci_lazy_methods_needed.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Context-insensitive lazy methods container
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "ci_lazy_methods_needed.h"
13 
15 
16 #include <util/namespace.h>
17 #include <util/std_types.h>
18 
19 #include <string>
20 
22 #include "select_pointer_type.h"
23 
28  const irep_idt &method_symbol_name)
29 {
30  callable_methods.insert(method_symbol_name);
31 }
32 
42 {
43  const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id);
44  if(symbol_table.symbols.count(clinit_wrapper))
45  add_needed_method(clinit_wrapper);
46 }
47 
52  const irep_idt &class_id)
53 {
54  resolve_inherited_componentt resolve_inherited_component{symbol_table};
56  cprover_nondet_initialize = resolve_inherited_component(
57  class_id, "cproverNondetInitialize:()V", true);
58 
59  if(cprover_nondet_initialize)
60  {
62  cprover_nondet_initialize->get_full_component_identifier());
63  }
64 }
65 
72  const irep_idt &class_symbol_name)
73 {
74  if(!instantiated_classes.insert(class_symbol_name).second)
75  return false;
76 
78 
79  // Special case for enums. We may want to generalise this, the comment in
80  // \ref java_object_factoryt::gen_nondet_pointer_init (TG-4689).
82  const auto &class_type =
83  to_java_class_type(ns.lookup(class_symbol_name).type);
84  if(class_type.get_base("java::java.lang.Enum"))
85  add_clinit_call(class_symbol_name);
86 
87  return true;
88 }
89 
95 {
97 
99 
100  // TODO we should be passing here a map that maps generic parameters
101  // to concrete types in the current context TG-2664
102  const pointer_typet &subbed_pointer_type =
104 
105  if(subbed_pointer_type != pointer_type)
106  {
107  initialize_instantiated_classes_from_pointer(subbed_pointer_type, ns);
108  }
109 }
110 
117  const namespacet &ns)
118 {
119  const auto &class_type = to_struct_tag_type(pointer_type.subtype());
120  const auto &param_classid = class_type.get_identifier();
121 
122  // Note here: different arrays may have different element types, so we should
123  // explore again even if we've seen this classid before in the array case.
124  if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
125  {
127  }
128 
130  {
131  // Assume if this is a generic like X<A, B, C>, then any concrete parameters
132  // will at some point be instantiated.
133  const auto &generic_args =
135  for(const auto &generic_arg : generic_args)
136  {
137  if(!is_java_generic_parameter(generic_arg))
138  add_all_needed_classes(generic_arg);
139  }
140  }
141 }
142 
147  const typet &class_type,
148  const namespacet &ns)
149 {
150  const auto &underlying_type = to_struct_type(ns.follow(class_type));
151  if(is_java_array_tag(underlying_type.get_tag()))
152  {
153  // If class_type is not a symbol this may be a reference array,
154  // but we can't tell what type.
155  if(class_type.id() == ID_struct_tag)
156  {
157  const typet &element_type =
159  if(
160  element_type.id() == ID_pointer &&
161  element_type.subtype().id() != ID_empty)
162  {
163  // This is a reference array -- mark its element type available.
165  }
166  }
167  }
168  else
169  {
170  for(const auto &field : underlying_type.components())
171  {
172  if(field.type().id() == ID_struct || field.type().id() == ID_struct_tag)
173  gather_field_types(field.type(), ns);
174  else if(field.type().id() == ID_pointer)
175  {
176  if(field.type().subtype().id() == ID_struct_tag)
177  {
179  }
180  else
181  {
182  // If raw structs were possible this would lead to missed
183  // dependencies, as both array element and specialised generic type
184  // information cannot be obtained in this case.
185  // We should therefore only be skipping pointers such as the uint16t*
186  // in our internal String representation.
187  INVARIANT(
188  field.type().subtype().id() != ID_struct,
189  "struct types should be referred to by symbol at this stage");
190  }
191  }
192  }
193  }
194 }
java_static_initializers.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ci_lazy_methods_neededt::instantiated_classes
std::unordered_set< irep_idt > & instantiated_classes
Definition: ci_lazy_methods_needed.h:54
typet::subtype
const typet & subtype() const
Definition: type.h:47
ci_lazy_methods_neededt::pointer_type_selector
const select_pointer_typet & pointer_type_selector
Definition: ci_lazy_methods_needed.h:57
select_pointer_type.h
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
ci_lazy_methods_neededt::initialize_instantiated_classes_from_pointer
void initialize_instantiated_classes_from_pointer(const pointer_typet &pointer_type, const namespacet &ns)
Build up list of methods for types for a specific pointer type.
Definition: ci_lazy_methods_needed.cpp:115
typet
The type of an expression, extends irept.
Definition: type.h:29
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
ci_lazy_methods_neededt::add_needed_class
bool add_needed_class(const irep_idt &)
Notes class class_symbol_name will be instantiated, or a static field belonging to it will be accesse...
Definition: ci_lazy_methods_needed.cpp:71
namespace.h
resolve_inherited_component.h
Given a class and a component (either field or method), find the closest parent that defines that com...
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
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
java_generic_typet::generic_type_arguments
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:927
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
ci_lazy_methods_needed.h
Context-insensitive lazy methods container.
ci_lazy_methods_neededt::symbol_table
const symbol_tablet & symbol_table
Definition: ci_lazy_methods_needed.h:55
std_types.h
Pre-defined types.
is_java_generic_type
bool is_java_generic_type(const typet &type)
Definition: java_types.h:947
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
to_java_generic_type
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
ci_lazy_methods_neededt::add_cprover_nondet_initialize_if_it_exists
void add_cprover_nondet_initialize_if_it_exists(const irep_idt &class_id)
For a given class id, if cproverNondetInitialize exists on it or any of its ancestors then note that ...
Definition: ci_lazy_methods_needed.cpp:51
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
ci_lazy_methods_neededt::add_clinit_call
void add_clinit_call(const irep_idt &class_id)
For a given class id, note that its static initializer is needed.
Definition: ci_lazy_methods_needed.cpp:41
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
ci_lazy_methods_neededt::gather_field_types
void gather_field_types(const typet &class_type, const namespacet &ns)
For a given type, gather all fields referenced by that type.
Definition: ci_lazy_methods_needed.cpp:146
ci_lazy_methods_neededt::add_needed_method
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
Definition: ci_lazy_methods_needed.cpp:27
clinit_wrapper_name
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
Definition: java_static_initializers.cpp:65
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:584
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1488
ci_lazy_methods_neededt::add_all_needed_classes
void add_all_needed_classes(const pointer_typet &pointer_type)
Add to the needed classes all classes specified, the replacement type if it will be replaced,...
Definition: ci_lazy_methods_needed.cpp:93
ci_lazy_methods_neededt::callable_methods
std::unordered_set< irep_idt > & callable_methods
Definition: ci_lazy_methods_needed.h:50
validation_modet::INVARIANT
@ INVARIANT
resolve_inherited_componentt
Definition: resolve_inherited_component.h:22