cprover
java_static_initializers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Java Static Initializers
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
10 #define CPROVER_JAVA_BYTECODE_JAVA_STATIC_INITIALIZERS_H
11 
12 #include "assignments_from_json.h"
13 #include "ci_lazy_methods_needed.h"
15 #include "select_pointer_type.h"
16 #include "synthetic_methods_map.h"
17 
18 #include <unordered_set>
19 
20 #include <util/message.h>
21 #include <util/std_code.h>
22 #include <util/symbol_table.h>
23 
24 irep_idt clinit_wrapper_name(const irep_idt &class_name);
26 
27 bool is_clinit_wrapper_function(const irep_idt &function_id);
28 bool is_clinit_function(const irep_idt &function_id);
29 bool is_user_specified_clinit_function(const irep_idt &function_id);
30 
32  symbol_tablet &symbol_table,
33  synthetic_methods_mapt &synthetic_methods,
34  const bool thread_safe,
35  const bool is_user_clinit_needed);
36 
38  const irep_idt &function_id,
39  symbol_table_baset &symbol_table,
40  const bool nondet_static,
41  const bool replace_clinit,
42  const java_object_factory_parameterst &object_factory_parameters,
43  const select_pointer_typet &pointer_type_selector,
44  message_handlert &message_handler);
45 
47  const irep_idt &function_id,
48  symbol_table_baset &symbol_table,
49  const bool nondet_static,
50  const bool replace_clinit,
51  const java_object_factory_parameterst &object_factory_parameters,
52  const select_pointer_typet &pointer_type_selector,
53  message_handlert &message_handler);
54 
56 std::unordered_multimap<irep_idt, symbolt>
57 class_to_declared_symbols(const symbol_tablet &symbol_table);
58 
83  const irep_idt &class_id,
84  const json_objectt &static_values_json,
85  symbol_table_baset &symbol_table,
86  optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
87  size_t max_user_array_length,
88  std::unordered_map<std::string, object_creation_referencet> &references,
89  const std::unordered_multimap<irep_idt, symbolt>
90  &class_to_declared_symbols_map);
91 
93 {
95  typedef std::unordered_multimap<irep_idt, irep_idt> stub_globals_by_classt;
97 
98 public:
100  symbol_tablet &symbol_table,
101  const std::unordered_set<irep_idt> &stub_globals_set,
102  synthetic_methods_mapt &synthetic_methods);
103 
105  const irep_idt &function_id,
106  symbol_table_baset &symbol_table,
107  const java_object_factory_parameterst &object_factory_parameters,
108  const select_pointer_typet &pointer_type_selector,
109  message_handlert &message_handler);
110 };
111 
113  symbol_tablet &symbol_table,
114  const std::unordered_set<irep_idt> &stub_globals_set,
115  const java_object_factory_parameterst &object_factory_parameters,
116  const select_pointer_typet &pointer_type_selector);
117 
118 #endif
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
class_to_declared_symbols
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
Definition: java_static_initializers.cpp:772
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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
stub_global_initializer_factoryt::get_stub_initializer_body
code_blockt get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
Definition: java_static_initializers.cpp:999
select_pointer_type.h
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
java_object_factory_parameters.h
is_clinit_wrapper_function
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
Definition: java_static_initializers.cpp:78
synthetic_methods_mapt
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Definition: synthetic_methods_map.h:53
stub_global_initializer_factoryt
Definition: java_static_initializers.h:93
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:746
nondet_static
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Definition: nondet_static.cpp:79
json_objectt
Definition: json.h:300
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
ci_lazy_methods_needed.h
Context-insensitive lazy methods container.
select_pointer_typet
Definition: select_pointer_type.h:26
create_static_initializer_symbols
void create_static_initializer_symbols(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe, const bool is_user_clinit_needed)
Create static initializer wrappers and possibly user-specified functions for initial static field val...
Definition: java_static_initializers.cpp:867
create_stub_global_initializers
void create_stub_global_initializers(symbol_tablet &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
message_handlert
Definition: message.h:28
get_user_specified_clinit_body
code_blockt get_user_specified_clinit_body(const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references, const std::unordered_multimap< irep_idt, symbolt > &class_to_declared_symbols_map)
Create the body of a user_specified_clinit function for a given class, which includes assignments for...
Definition: java_static_initializers.cpp:784
user_specified_clinit_name
irep_idt user_specified_clinit_name(const irep_idt &class_name)
Definition: java_static_initializers.cpp:70
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
get_clinit_wrapper_body
code_ifthenelset get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Produces the static initializer wrapper body for the given function.
Definition: java_static_initializers.cpp:712
assignments_from_json.h
stub_global_initializer_factoryt::create_stub_global_initializer_symbols
void create_stub_global_initializer_symbols(symbol_tablet &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, synthetic_methods_mapt &synthetic_methods)
Create static initializer symbols for each distinct class that has stub globals.
Definition: java_static_initializers.cpp:918
is_clinit_function
bool is_clinit_function(const irep_idt &function_id)
Check if function_id is a clinit.
Definition: java_static_initializers.cpp:86
stub_global_initializer_factoryt::stub_globals_by_class
stub_globals_by_classt stub_globals_by_class
Definition: java_static_initializers.h:96
is_user_specified_clinit_function
bool is_user_specified_clinit_function(const irep_idt &function_id)
Check if function_id is a user-specified clinit.
Definition: java_static_initializers.cpp:94
symbol_table.h
Author: Diffblue Ltd.
message.h
stub_global_initializer_factoryt::stub_globals_by_classt
std::unordered_multimap< irep_idt, irep_idt > stub_globals_by_classt
Maps class symbols onto the stub globals that belong to them.
Definition: java_static_initializers.h:95
get_thread_safe_clinit_wrapper_body
code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Thread safe version of the static initializer.
Definition: java_static_initializers.cpp:516
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
synthetic_methods_map.h
Synthetic methods are particular methods internally generated by the Java frontend,...