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 
13 #include "select_pointer_type.h"
14 #include "synthetic_methods_map.h"
15 
16 #include <unordered_set>
17 
18 #include <util/symbol_table.h>
19 #include <util/std_code.h>
20 
21 irep_idt clinit_wrapper_name(const irep_idt &class_name);
22 
23 bool is_clinit_wrapper_function(const irep_idt &function_id);
24 
26  symbol_tablet &symbol_table,
27  synthetic_methods_mapt &synthetic_methods,
28  const bool thread_safe);
29 
31  const irep_idt &function_id,
32  symbol_table_baset &symbol_table,
33  const bool nondet_static,
34  const java_object_factory_parameterst &object_factory_parameters,
35  const select_pointer_typet &pointer_type_selector);
36 
38  const irep_idt &function_id,
39  symbol_table_baset &symbol_table,
40  const bool nondet_static,
41  const java_object_factory_parameterst &object_factory_parameters,
42  const select_pointer_typet &pointer_type_selector);
43 
45 {
47  typedef std::unordered_multimap<irep_idt, irep_idt> stub_globals_by_classt;
49 
50 public:
52  symbol_tablet &symbol_table,
53  const std::unordered_set<irep_idt> &stub_globals_set,
54  synthetic_methods_mapt &synthetic_methods);
55 
57  const irep_idt &function_id,
58  symbol_table_baset &symbol_table,
59  const java_object_factory_parameterst &object_factory_parameters,
60  const select_pointer_typet &pointer_type_selector);
61 };
62 
64  symbol_tablet &symbol_table,
65  const std::unordered_set<irep_idt> &stub_globals_set,
66  const java_object_factory_parameterst &object_factory_parameters,
67  const select_pointer_typet &pointer_type_selector);
68 
69 #endif
code_blockt get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Thread safe version of the static initializer.
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)
void create_static_initializer_wrappers(symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Create static initializer wrappers for all classes that need them.
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_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
The symbol table.
Definition: symbol_table.h:19
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Author: Diffblue Ltd.
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.
stub_globals_by_classt stub_globals_by_class
The symbol table base class interface.
Synthetic methods are particular methods internally generated by the Java frontend, including thunks to ensure static initializers are run once and initializers created for unknown / stub types.
std::unordered_multimap< irep_idt, irep_idt > stub_globals_by_classt
Maps class symbols onto the stub globals that belong to them.
A codet representing sequential composition of program statements.
Definition: std_code.h:150
codet representation of an if-then-else statement.
Definition: std_code.h:614
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)
Create the body of a synthetic static initializer (clinit method), which initialise stub globals in t...
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
code_ifthenelset get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Produces the static initializer wrapper body for the given function.