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.
value = value;
99 new_symbol.
mode = ID_java;
100 symbol_table.
add(new_symbol);
110 return id2string(class_name) +
"::clinit_already_run";
194 const auto base_name =
to_symbol_type(base.type()).get_identifier();
196 auto findit = symbol_table.
symbols.find(base_init_routine);
197 if(findit == symbol_table.
symbols.end())
200 call_base.
function() = findit->second.symbol_expr();
205 auto find_sym_it = symbol_table.
symbols.find(real_clinit_name);
206 if(find_sym_it != symbol_table.
symbols.end())
209 call_real_init.
function() = find_sym_it->second.symbol_expr();
254 const bool thread_safe)
299 wrapper_method_symbol.
base_name =
"clinit_wrapper";
300 wrapper_method_symbol.
type = wrapper_method_type;
304 wrapper_method_symbol.
type.
set(ID_C_class, class_name);
305 wrapper_method_symbol.
mode = ID_java;
306 bool failed = symbol_table.
add(wrapper_method_symbol);
307 INVARIANT(!failed,
"clinit-wrapper symbol should be fresh");
309 auto insert_result = synthetic_methods.emplace(
310 wrapper_method_symbol.
name,
313 insert_result.second,
314 "synthetic methods map should not already contain entry for " 392 !class_name.
empty(),
"wrapper function should be annotated with its class");
394 const symbolt &clinit_state_sym =
396 const symbolt &clinit_thread_local_state_sym =
411 codet atomic_begin(ID_atomic_begin);
412 codet atomic_end(ID_atomic_end);
430 "Automatically generated function. States are:\n" 431 " 0 = class not initialized, init val of clinit_state/clinit_local_state\n" 432 " 1 = class initialization in progress, by this or another thread\n" 433 " 2 = initialization finished with success, by this or another thread\n";
442 function_body.
add(decl);
452 function_body.
add(conditional);
460 function_body.
add(assign);
465 function_body.
add(atomic_begin);
474 function_body.
add(assume);
495 not_init_conditional.
then_case() = then_block;
501 init_conditional_body.
add(
503 init_conditional.
then_case() = init_conditional_body;
504 not_init_conditional.
else_case() = init_conditional;
505 function_body.
add(not_init_conditional);
510 function_body.
add(atomic_end);
518 function_body.
add(conditional);
539 function_body.
append(init_body);
548 function_body.
add(atomic_begin);
552 function_body.
add(atomic_end);
556 return function_body;
591 !class_name.
empty(),
"wrapper function should be annotated with its class");
593 const symbolt &already_run_symbol =
597 already_run_symbol.symbol_expr(),
604 wrapper_body.
cond() = check_already_run;
613 wrapper_body.then_case() = init_body;
629 const bool thread_safe)
636 std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
639 for(
const auto node : topsorted_nodes)
641 const irep_idt &class_identifier = class_graph[node].class_identifier;
645 class_identifier, symbol_table, synthetic_methods, thread_safe);
653 template<
class itertype>
657 auto initial_key = in->first;
658 while(in != end && in->first == initial_key)
673 const std::unordered_set<irep_idt> &stub_globals_set,
677 for(
const irep_idt &stub_global : stub_globals_set)
692 global_symbol.
type.
get(ID_C_class);
695 "static field should be annotated with its defining class");
710 "only incomplete classes should be given synthetic static initialisers");
713 "a class cannot be both incomplete, and so have stub static fields, and " 714 "also define a static initializer");
719 static_init_symbol.
name = static_init_name;
720 static_init_symbol.pretty_name = static_init_name;
721 static_init_symbol.base_name =
"clinit():V";
722 static_init_symbol.mode = ID_java;
723 static_init_symbol.type = thunk_type;
727 static_init_symbol.type.set(ID_C_class, it->first);
729 bool failed = symbol_table.
add(static_init_symbol);
730 INVARIANT(!failed,
"symbol should not already exist");
732 auto insert_result = synthetic_methods.emplace(
733 static_init_symbol.name,
736 insert_result.second,
737 "synthetic methods map should not already contain entry for " 738 "stub static initializer");
765 "synthetic static initializer should be annotated with its class");
774 class_globals.first != class_globals.second,
775 "class with synthetic clinit should have at least one global to init");
780 for(
auto it = class_globals.first; it != class_globals.second; ++it)
798 pointer_type_selector,
802 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...
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...