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 #include <util/symbol_table.h>
19 
22 #include "java_types.h"
23 #include "select_pointer_type.h"
24 
29  const irep_idt &method_symbol_name)
30 {
31  callable_methods.insert(method_symbol_name);
32 }
33 
43 {
44  const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id);
45  if(symbol_table.symbols.count(clinit_wrapper))
46  add_needed_method(clinit_wrapper);
47 }
48 
53  const irep_idt &class_id)
54 {
55  resolve_inherited_componentt resolve_inherited_component{symbol_table};
57  cprover_nondet_initialize = resolve_inherited_component(
58  class_id, "cproverNondetInitialize:()V", true);
59 
60  if(cprover_nondet_initialize)
61  {
63  cprover_nondet_initialize->get_full_component_identifier());
64  }
65 }
66 
73  const irep_idt &class_symbol_name)
74 {
75  if(!instantiated_classes.insert(class_symbol_name).second)
76  return false;
77 
79 
80  // Special case for enums. We may want to generalise this, the comment in
81  // \ref java_object_factoryt::gen_nondet_pointer_init (TG-4689).
83  const auto &class_type =
84  to_java_class_type(ns.lookup(class_symbol_name).type);
85  if(class_type.get_base("java::java.lang.Enum"))
86  add_clinit_call(class_symbol_name);
87 
88  return true;
89 }
90 
96 {
98 
100 
101  // TODO we should be passing here a map that maps generic parameters
102  // to concrete types in the current context TG-2664
103  const pointer_typet &subbed_pointer_type =
105 
106  if(subbed_pointer_type != pointer_type)
107  {
108  initialize_instantiated_classes_from_pointer(subbed_pointer_type, ns);
109  }
110 }
111 
118  const namespacet &ns)
119 {
120  const auto &class_type = to_struct_tag_type(pointer_type.subtype());
121  const auto &param_classid = class_type.get_identifier();
122 
123  // Note here: different arrays may have different element types, so we should
124  // explore again even if we've seen this classid before in the array case.
125  if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
126  {
128  }
129 
131  {
132  // Assume if this is a generic like X<A, B, C>, then any concrete parameters
133  // will at some point be instantiated.
134  const auto &generic_args =
136  for(const auto &generic_arg : generic_args)
137  {
138  if(!is_java_generic_parameter(generic_arg))
139  add_all_needed_classes(generic_arg);
140  }
141  }
142 }
143 
148  const typet &class_type,
149  const namespacet &ns)
150 {
151  const auto &underlying_type = to_struct_type(ns.follow(class_type));
152  if(is_java_array_tag(underlying_type.get_tag()))
153  {
154  // If class_type is not a symbol this may be a reference array,
155  // but we can't tell what type.
156  if(class_type.id() == ID_struct_tag)
157  {
158  const typet &element_type =
160  if(
161  element_type.id() == ID_pointer &&
162  element_type.subtype().id() != ID_empty)
163  {
164  // This is a reference array -- mark its element type available.
166  }
167  }
168  }
169  else
170  {
171  for(const auto &field : underlying_type.components())
172  {
173  if(field.type().id() == ID_struct || field.type().id() == ID_struct_tag)
174  gather_field_types(field.type(), ns);
175  else if(field.type().id() == ID_pointer)
176  {
177  if(field.type().subtype().id() == ID_struct_tag)
178  {
180  }
181  else
182  {
183  // If raw structs were possible this would lead to missed
184  // dependencies, as both array element and specialised generic type
185  // information cannot be obtained in this case.
186  // We should therefore only be skipping pointers such as the uint16t*
187  // in our internal String representation.
188  INVARIANT(
189  field.type().subtype().id() != ID_struct,
190  "struct types should be referred to by symbol at this stage");
191  }
192  }
193  }
194  }
195 }
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
Context-insensitive lazy methods container.
std::unordered_set< irep_idt > & instantiated_classes
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.
const select_pointer_typet & pointer_type_selector
void gather_field_types(const typet &class_type, const namespacet &ns)
For a given type, gather all fields referenced by that type.
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
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,...
std::unordered_set< irep_idt > & callable_methods
const symbol_tablet & symbol_table
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...
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 ...
void add_clinit_call(const irep_idt &class_id)
For a given class id, note that its static initializer is needed.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const irep_idt & id() const
Definition: irep.h:407
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:925
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
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 symbolst & symbols
Read-only field, used to look up symbols given their names.
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
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...
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
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:231
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
bool is_java_generic_type(const typet &type)
Definition: java_types.h:945
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_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:952
nonstd::optional< T > optionalt
Definition: optional.h:35
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
Given a class and a component (either field or method), find the closest parent that defines that com...
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
Pre-defined types.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
Author: Diffblue Ltd.