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.h"
14 
16 #include <string>
17 #include <util/namespace.h>
18 #include <util/std_types.h>
19 
24  const irep_idt &method_symbol_name)
25 {
26  callable_methods.insert(method_symbol_name);
27 }
28 
39  const irep_idt &class_id,
40  const symbol_tablet &symbol_table)
41 {
42  const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id);
43  if(symbol_table.symbols.count(clinit_wrapper))
44  add_needed_method(clinit_wrapper);
45 }
46 
53  const irep_idt &class_symbol_name)
54 {
55  if(!instantiated_classes.insert(class_symbol_name).second)
56  return false;
57 
58  const std::string &class_name_string = id2string(class_symbol_name);
59  const irep_idt cprover_validate(
60  class_name_string + ".cproverNondetInitialize:()V");
61  if(symbol_table.symbols.count(cprover_validate))
62  add_needed_method(cprover_validate);
63 
64  // Special case for enums. We may want to generalise this, the comment in
65  // \ref java_object_factoryt::gen_nondet_pointer_init (TG-4689).
67  const auto &class_type =
68  to_java_class_type(ns.lookup(class_symbol_name).type);
69  if(class_type.get_base("java::java.lang.Enum"))
70  add_clinit_call(class_symbol_name, symbol_table);
71 
72  return true;
73 }
74 
80 {
82 
84 
85  // TODO we should be passing here a map that maps generic parameters
86  // to concrete types in the current context TG-2664
87  const pointer_typet &subbed_pointer_type =
89 
90  if(subbed_pointer_type != pointer_type)
91  {
92  initialize_instantiated_classes_from_pointer(subbed_pointer_type, ns);
93  }
94 }
95 
102  const namespacet &ns)
103 {
104  const auto &class_type = to_struct_tag_type(pointer_type.subtype());
105  const auto &param_classid = class_type.get_identifier();
106 
107  // Note here: different arrays may have different element types, so we should
108  // explore again even if we've seen this classid before in the array case.
109  if(add_needed_class(param_classid) || is_java_array_tag(param_classid))
110  {
112  }
113 
115  {
116  // Assume if this is a generic like X<A, B, C>, then any concrete parameters
117  // will at some point be instantiated.
118  const auto &generic_args =
120  for(const auto &generic_arg : generic_args)
121  {
122  if(!is_java_generic_parameter(generic_arg))
123  add_all_needed_classes(generic_arg);
124  }
125  }
126 }
127 
132  const typet &class_type,
133  const namespacet &ns)
134 {
135  const auto &underlying_type = to_struct_type(ns.follow(class_type));
136  if(is_java_array_tag(underlying_type.get_tag()))
137  {
138  // If class_type is not a symbol this may be a reference array,
139  // but we can't tell what type.
140  if(class_type.id() == ID_struct_tag)
141  {
142  const typet &element_type =
144  if(element_type.id() == ID_pointer)
145  {
146  // This is a reference array -- mark its element type available.
148  }
149  }
150  }
151  else
152  {
153  for(const auto &field : underlying_type.components())
154  {
155  if(field.type().id() == ID_struct || field.type().id() == ID_struct_tag)
156  gather_field_types(field.type(), ns);
157  else if(field.type().id() == ID_pointer)
158  {
159  if(field.type().subtype().id() == ID_struct_tag)
160  {
162  }
163  else
164  {
165  // If raw structs were possible this would lead to missed
166  // dependencies, as both array element and specialised generic type
167  // information cannot be obtained in this case.
168  // We should therefore only be skipping pointers such as the uint16t*
169  // in our internal String representation.
170  INVARIANT(
171  field.type().subtype().id() != ID_struct,
172  "struct types should be referred to by symbol at this stage");
173  }
174  }
175  }
176  }
177 }
The type of an expression, extends irept.
Definition: type.h:27
const irep_idt & get_identifier() const
Definition: std_types.h:479
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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
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
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:173
const select_pointer_typet & pointer_type_selector
void add_clinit_call(const irep_idt &class_id, const symbol_tablet &symbol_table)
For a given class id, note that its static initializer is needed.
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:495
const irep_idt & id() const
Definition: irep.h:259
std::unordered_set< irep_idt > & instantiated_classes
The pointer type These are both &#39;bitvector_typet&#39; (they have a width) and &#39;type_with_subtypet&#39; (they ...
Definition: std_types.h:1507
The symbol table.
Definition: symbol_table.h:19
Collect methods needed to be loaded using the lazy method.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void add_needed_method(const irep_idt &)
Notes method_symbol_name is referenced from some reachable function, and should therefore be elaborat...
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const symbolst & symbols
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 java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:524
Pre-defined types.
void gather_field_types(const typet &class_type, const namespacet &ns)
For a given type, gather all fields referenced by that type.
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...
std::unordered_set< irep_idt > & callable_methods
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...
bool is_java_generic_type(const typet &type)
Definition: java_types.h:517
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.
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...
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:246