CBMC
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 "synthetic_methods_map.h"
13 
14 #include <unordered_set>
15 
16 #include <util/std_code.h>
17 
19 class json_objectt;
20 class message_handlert;
22 class symbol_table_baset;
23 class symbolt;
26 
27 irep_idt clinit_wrapper_name(const irep_idt &class_name);
29 
30 bool is_clinit_wrapper_function(const irep_idt &function_id);
31 bool is_clinit_function(const irep_idt &function_id);
32 bool is_user_specified_clinit_function(const irep_idt &function_id);
33 
35  symbol_table_baset &symbol_table,
36  synthetic_methods_mapt &synthetic_methods,
37  const bool thread_safe,
38  const bool is_user_clinit_needed);
39 
41  const irep_idt &function_id,
42  symbol_table_baset &symbol_table,
43  const bool nondet_static,
44  const bool replace_clinit,
45  const java_object_factory_parameterst &object_factory_parameters,
46  const select_pointer_typet &pointer_type_selector,
47  message_handlert &message_handler);
48 
50  const irep_idt &function_id,
51  symbol_table_baset &symbol_table,
52  const bool nondet_static,
53  const bool replace_clinit,
54  const java_object_factory_parameterst &object_factory_parameters,
55  const select_pointer_typet &pointer_type_selector,
56  message_handlert &message_handler);
57 
59 std::unordered_multimap<irep_idt, symbolt>
61 
86  const irep_idt &class_id,
87  const json_objectt &static_values_json,
88  symbol_table_baset &symbol_table,
89  std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
90  size_t max_user_array_length,
91  std::unordered_map<std::string, object_creation_referencet> &references,
92  const std::unordered_multimap<irep_idt, symbolt>
93  &class_to_declared_symbols_map);
94 
96 {
98  typedef std::unordered_multimap<irep_idt, irep_idt> stub_globals_by_classt;
100 
101 public:
103  symbol_table_baset &symbol_table,
104  const std::unordered_set<irep_idt> &stub_globals_set,
105  synthetic_methods_mapt &synthetic_methods);
106 
108  const irep_idt &function_id,
109  symbol_table_baset &symbol_table,
110  const java_object_factory_parameterst &object_factory_parameters,
111  const select_pointer_typet &pointer_type_selector,
112  message_handlert &message_handler);
113 };
114 
116  symbol_table_baset &symbol_table,
117  const std::unordered_set<irep_idt> &stub_globals_set,
118  const java_object_factory_parameterst &object_factory_parameters,
119  const select_pointer_typet &pointer_type_selector);
120 
121 #endif
A codet representing sequential composition of program statements.
Definition: std_code.h:130
codet representation of an if-then-else statement.
Definition: std_code.h:460
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
void create_stub_global_initializer_symbols(symbol_table_baset &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.
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...
std::unordered_multimap< irep_idt, irep_idt > stub_globals_by_classt
Maps class symbols onto the stub globals that belong to them.
stub_globals_by_classt stub_globals_by_class
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
code_blockt get_user_specified_clinit_body(const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, std::optional< 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...
void create_static_initializer_symbols(symbol_table_baset &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...
void create_stub_global_initializers(symbol_table_baset &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)
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.
bool is_user_specified_clinit_function(const irep_idt &function_id)
Check if function_id is a user-specified clinit.
irep_idt user_specified_clinit_name(const irep_idt &class_name)
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_table_baset &symbol_table)
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.
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
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_function(const irep_idt &function_id)
Check if function_id is a clinit.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Information to store when several references point to the same Java object.
Synthetic methods are particular methods internally generated by the Java frontend,...
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.