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";
195 const auto base_name =
to_symbol_type(base.type()).get_identifier();
197 auto findit = symbol_table.
symbols.find(base_init_routine);
198 if(findit == symbol_table.
symbols.end())
201 call_base.
function() = findit->second.symbol_expr();
206 auto find_sym_it = symbol_table.
symbols.find(real_clinit_name);
207 if(find_sym_it != symbol_table.
symbols.end())
210 call_real_init.
function() = find_sym_it->second.symbol_expr();
255 const bool thread_safe)
300 wrapper_method_symbol.
base_name =
"clinit_wrapper";
301 wrapper_method_symbol.
type = wrapper_method_type;
305 wrapper_method_symbol.
type.
set(ID_C_class, class_name);
306 wrapper_method_symbol.
mode = ID_java;
307 bool failed = symbol_table.
add(wrapper_method_symbol);
308 INVARIANT(!failed,
"clinit-wrapper symbol should be fresh");
310 auto insert_result = synthetic_methods.emplace(
311 wrapper_method_symbol.
name,
314 insert_result.second,
315 "synthetic methods map should not already contain entry for " 393 !class_name.
empty(),
"wrapper function should be annotated with its class");
395 const symbolt &clinit_state_sym =
397 const symbolt &clinit_thread_local_state_sym =
412 codet atomic_begin(ID_atomic_begin);
413 codet atomic_end(ID_atomic_end);
431 "Automatically generated function. States are:\n" 432 " 0 = class not initialized, init val of clinit_state/clinit_local_state\n" 433 " 1 = class initialization in progress, by this or another thread\n" 434 " 2 = initialization finished with success, by this or another thread\n";
443 function_body.
add(decl);
453 function_body.
add(conditional);
461 function_body.
add(assign);
466 function_body.
add(atomic_begin);
475 function_body.
add(assume);
496 not_init_conditional.
then_case() = then_block;
502 init_conditional_body.
add(
504 init_conditional.
then_case() = init_conditional_body;
505 not_init_conditional.
else_case() = init_conditional;
506 function_body.
add(not_init_conditional);
511 function_body.
add(atomic_end);
519 function_body.
add(conditional);
540 function_body.
append(init_body);
549 function_body.
add(atomic_begin);
553 function_body.
add(atomic_end);
557 return function_body;
592 !class_name.
empty(),
"wrapper function should be annotated with its class");
594 const symbolt &already_run_symbol =
598 already_run_symbol.symbol_expr(),
605 wrapper_body.
cond() = check_already_run;
614 wrapper_body.then_case() = init_body;
630 const bool thread_safe)
637 std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
640 for(
const auto node : topsorted_nodes)
642 const irep_idt &class_identifier = class_graph[node].class_identifier;
646 class_identifier, symbol_table, synthetic_methods, thread_safe);
654 template<
class itertype>
658 auto initial_key = in->first;
659 while(in != end && in->first == initial_key)
674 const std::unordered_set<irep_idt> &stub_globals_set,
678 for(
const irep_idt &stub_global : stub_globals_set)
693 global_symbol.
type.
get(ID_C_class);
696 "static field should be annotated with its defining class");
711 "only incomplete classes should be given synthetic static initialisers");
714 "a class cannot be both incomplete, and so have stub static fields, and " 715 "also define a static initializer");
720 static_init_symbol.
name = static_init_name;
721 static_init_symbol.pretty_name = static_init_name;
722 static_init_symbol.base_name =
"clinit():V";
723 static_init_symbol.mode = ID_java;
724 static_init_symbol.type = thunk_type;
728 static_init_symbol.type.set(ID_C_class, it->first);
730 bool failed = symbol_table.
add(static_init_symbol);
731 INVARIANT(!failed,
"symbol should not already exist");
733 auto insert_result = synthetic_methods.emplace(
734 static_init_symbol.name,
737 insert_result.second,
738 "synthetic methods map should not already contain entry for " 739 "stub static initializer");
766 "synthetic static initializer should be annotated with its class");
775 class_globals.first != class_globals.second,
776 "class with synthetic clinit should have at least one global to init");
781 for(
auto it = class_globals.first; it != class_globals.second; ++it)
801 pointer_type_selector,
805 return static_init_body;
The type of an expression.
irep_idt name
The unique identifier.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
const codet & then_case() const
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)
const exprt & cond() const
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...
void move_to_operands(exprt &expr)
static irep_idt clinit_function_name(const irep_idt &class_name)
Get name of the real static initializer for a given class.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
exprt value
Initial value of symbol.
codet get_thread_safe_clinit_wrapper_body(const irep_idt &function_id, symbol_table_baset &symbol_table)
Thread safe version of the static initialiser.
irep_idt pretty_name
Language-specific display name.
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
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.
bool get_bool(const irep_namet &name) const
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.
#define INVARIANT(CONDITION, REASON)
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.
A 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)
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...
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
#define PRECONDITION(CONDITION)
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.
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 void clinit_wrapper_do_recursive_calls(const symbol_tablet &symbol_table, const irep_idt &class_name, code_blockt &init_body)
Generates codet that iterates through the base types of the class specified by class_name, C, and recursively adds calls to their clinit wrapper.
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.
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
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...
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 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...
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.
const basest & bases() const
source_locationt & add_source_location()
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.
A statement in a programming language.
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
const codet & else_case() const
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...
void set(const irep_namet &name, const irep_idt &value)
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.
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...