86 const bool is_thread_local,
87 const bool is_static_lifetime)
90 new_symbol.
name = name;
93 new_symbol.
type = type;
94 new_symbol.
type.
set(ID_C_no_nondet_initialization,
true);
95 new_symbol.
value = value;
100 new_symbol.
mode = ID_java;
101 symbol_table.
add(new_symbol);
111 return id2string(class_name) +
"::clinit_already_run";
206 const auto base_name = base.
type().get_identifier();
208 auto findit = symbol_table.
symbols.find(base_init_routine);
209 if(findit == symbol_table.
symbols.end())
213 init_body.
add(call_base);
217 auto find_sym_it = symbol_table.
symbols.find(real_clinit_name);
218 if(find_sym_it != symbol_table.
symbols.end())
221 init_body.
add(call_real_init);
232 std::vector<irep_idt> nondet_ids;
236 [&](
const std::pair<irep_idt, symbolt> &symbol) {
238 symbol.second.type.get(ID_C_class) == class_name &&
239 symbol.second.is_static_lifetime &&
240 !symbol.second.type.get_bool(ID_C_constant))
242 nondet_ids.push_back(symbol.first);
246 for(
const auto &
id : nondet_ids)
264 pointer_type_selector,
310 const bool thread_safe)
355 wrapper_method_symbol.
base_name =
"clinit_wrapper";
356 wrapper_method_symbol.
type = wrapper_method_type;
360 wrapper_method_symbol.
type.
set(ID_C_class, class_name);
361 wrapper_method_symbol.
mode = ID_java;
362 bool failed = symbol_table.
add(wrapper_method_symbol);
363 INVARIANT(!failed,
"clinit-wrapper symbol should be fresh");
365 auto insert_result = synthetic_methods.emplace(
366 wrapper_method_symbol.
name,
369 insert_result.second,
370 "synthetic methods map should not already contain entry for " 458 !class_name.
empty(),
"wrapper function should be annotated with its class");
460 const symbolt &clinit_state_sym =
462 const symbolt &clinit_thread_local_state_sym =
477 codet atomic_begin(ID_atomic_begin);
478 codet atomic_end(ID_atomic_end);
496 "Automatically generated function. States are:\n" 497 " 0 = class not initialized, init val of clinit_state/clinit_local_state\n" 498 " 1 = class initialization in progress, by this or another thread\n" 499 " 2 = initialization finished with success, by this or another thread\n";
508 function_body.
add(decl);
518 function_body.
add(std::move(conditional));
526 function_body.
add(assign);
531 function_body.
add(atomic_begin);
540 function_body.
add(assume);
565 std::move(init_conditional));
567 function_body.
add(std::move(not_init_conditional));
572 function_body.
add(atomic_end);
578 function_body.
add(std::move(conditional));
604 object_factory_parameters,
605 pointer_type_selector);
606 function_body.
append(init_body);
615 function_body.
add(atomic_begin);
619 function_body.
add(atomic_end);
623 return function_body;
668 !class_name.
empty(),
"wrapper function should be annotated with its class");
670 const symbolt &already_run_symbol =
674 already_run_symbol.symbol_expr(),
686 object_factory_parameters,
687 pointer_type_selector);
690 return code_ifthenelset(std::move(check_already_run), std::move(init_body));
704 const bool thread_safe)
711 std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
714 for(
const auto node : topsorted_nodes)
716 const irep_idt &class_identifier = class_graph[node].class_identifier;
720 class_identifier, symbol_table, synthetic_methods, thread_safe);
728 template<
class itertype>
732 auto initial_key = in->first;
733 while(in != end && in->first == initial_key)
748 const std::unordered_set<irep_idt> &stub_globals_set,
752 for(
const irep_idt &stub_global : stub_globals_set)
767 global_symbol.
type.
get(ID_C_class);
770 "static field should be annotated with its defining class");
785 "only stub classes should be given synthetic static initialisers");
788 "a class cannot be both incomplete, and so have stub static fields, and " 789 "also define a static initializer");
794 static_init_symbol.
name = static_init_name;
795 static_init_symbol.pretty_name = static_init_name;
796 static_init_symbol.base_name =
"clinit():V";
797 static_init_symbol.mode = ID_java;
798 static_init_symbol.type = thunk_type;
802 static_init_symbol.type.set(ID_C_class, it->first);
804 bool failed = symbol_table.
add(static_init_symbol);
805 INVARIANT(!failed,
"symbol should not already exist");
807 auto insert_result = synthetic_methods.emplace(
808 static_init_symbol.name,
811 insert_result.second,
812 "synthetic methods map should not already contain entry for " 813 "stub static initializer");
840 "synthetic static initializer should be annotated with its class");
849 class_globals.first != class_globals.second,
850 "class with synthetic clinit should have at least one global to init");
855 for(
auto it = class_globals.first; it != class_globals.second; ++it)
875 pointer_type_selector,
879 return static_init_body;
The void type, the same as empty_typet.
The type of an expression, extends irept.
irep_idt name
The unique identifier.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
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.
void set_function(const irep_idt &function)
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
static void create_clinit_wrapper_symbols(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods, const bool thread_safe)
Creates a static initializer wrapper symbol for the given class, along with a global boolean that tra...
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
irep_idt mode
Language mode.
std::string comment(const rw_set_baset::entryt &entry, bool write)
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.
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
static irep_idt clinit_function_name(const irep_idt &class_name)
Get name of the real static initializer for a given class.
exprt value
Initial value of symbol.
irep_idt pretty_name
Language-specific display name.
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
A constant literal expression.
static irep_idt clinit_local_init_complete_var_name(const irep_idt &class_name)
Get name of the static-initialization local variable for a given class.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
static irep_idt clinit_state_var_name(const irep_idt &class_name)
Get name of the static-initialization-state global variable for a given class.
const typet clinit_states_type
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
The Boolean constant true.
static void clinit_wrapper_do_recursive_calls(symbol_table_baset &symbol_table, const irep_idt &class_name, code_blockt &init_body, const bool nondet_static, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Generates codet that iterates through the base types of the class specified by class_name,...
const basest & bases() const
Get the collection of base classes/structs.
A codet representing the declaration of a local variable.
const std::string clinit_function_suffix
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
void set_file(const irep_idt &file)
API to expression classes.
static itertype advance_to_next_key(itertype in, itertype end)
Advance map iterator to next distinct key.
const irep_idt & get(const irep_namet &name) const
void set_line(const irep_idt &line)
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
#define PRECONDITION(CONDITION)
codet representation of a function call statement.
std::list< node_indext > topsort() const
Find a topological order of the nodes if graph is DAG, return empty list for non-DAG or empty graph.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static bool needs_clinit_wrapper(const irep_idt &class_name, const symbol_tablet &symbol_table)
Checks whether a static initializer wrapper is needed for a given class, i.e.
const std::string clinit_wrapper_suffix
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
The Boolean constant false.
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.
static symbolt add_new_variable_symbol(symbol_table_baset &symbol_table, const irep_idt &name, const typet &type, const exprt &value, const bool is_thread_local, const bool is_static_lifetime)
Add a new symbol to the symbol table.
An assumption, which must hold in subsequent code.
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.
static irep_idt clinit_already_run_variable_name(const irep_idt &class_name)
Get name of the static-initialization-already-done global variable for a given class.
typet type
Type of symbol.
Allocate dynamic objects (using MALLOC)
stub_globals_by_classt stub_globals_by_class
Base class or struct that a class or struct inherits from.
static code_assignt gen_clinit_assign(const exprt &expr, const clinit_statest state)
Generates a code_assignt for clinit_statest /param expr: expression to be used as the LHS of generate...
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
clinit_statest
The three states in which a <clinit> method for a class can be before, after, and during static class...
static irep_idt clinit_thread_local_state_var_name(const irep_idt &class_name)
Get name of the static-initialization-state local state variable for a given class.
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
codet representation of an if-then-else statement.
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...
Expression to hold a symbol (variable)
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
A generated (synthetic) static initializer function for a stub type.
bool has_suffix(const std::string &s, const std::string &suffix)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Data structure for representing an arbitrary statement in a program.
codet representation of a "return from a function" statement.
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...
const java_class_typet & to_java_class_type(const typet &type)
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
A codet representing an assignment in the program.
void set(const irep_namet &name, const irep_idt &value)
static equal_exprt gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
Generates an equal_exprt for clinit_statest /param expr: expression to be used as the LHS of generate...