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 
35  const irep_idt &function_id,
36  symbol_table_baset &symbol_table);
37 
39 {
41  typedef std::unordered_multimap<irep_idt, irep_idt> stub_globals_by_classt;
43 
44 public:
46  symbol_tablet &symbol_table,
47  const std::unordered_set<irep_idt> &stub_globals_set,
48  synthetic_methods_mapt &synthetic_methods);
49 
51  const irep_idt &function_id,
52  symbol_table_baset &symbol_table,
53  const object_factory_parameterst &object_factory_parameters,
54  const select_pointer_typet &pointer_type_selector);
55 };
56 
58  symbol_tablet &symbol_table,
59  const std::unordered_set<irep_idt> &stub_globals_set,
60  const object_factory_parameterst &object_factory_parameters,
61  const select_pointer_typet &pointer_type_selector);
62 
63 #endif
codet get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Thread safe version of the static initialiser.
codet get_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Produces the static initialiser wrapper body for the given function.
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
codet get_stub_initializer_body(const irep_idt &function_id, symbol_table_baset &symbol_table, const 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...
Author: Diffblue Ltd.
void create_stub_global_initializers(symbol_tablet &symbol_table, const std::unordered_set< irep_idt > &stub_globals_set, const object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
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.
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
A statement in a programming language.
Definition: std_code.h:21
Handle selection of correct pointer type (for example changing abstract classes to concrete versions)...