cprover
Loading...
Searching...
No Matches
ci_lazy_methods_needed.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Context-insensitive lazy methods container
4
5Author: Chris Smowton, chris.smowton@diffblue.com
6
7\*******************************************************************/
8
11
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.base_type());
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 to_pointer_type(element_type).base_type().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}
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
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:396
const generic_type_argumentst & generic_type_arguments() const
Definition: java_types.h:926
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
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
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:29
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...
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:231
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
const java_generic_typet & to_java_generic_type(const typet &type)
Definition: java_types.h:954
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:947
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:820
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:79
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)...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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.