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,...
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.