Go to the documentation of this file.
112 const bool is_thread_local,
113 const bool is_static_lifetime)
116 new_symbol.
name = name;
119 new_symbol.
type = type;
120 new_symbol.
type.
set(ID_C_no_nondet_initialization,
true);
121 new_symbol.
value = value;
126 new_symbol.
mode = ID_java;
127 symbol_table.
add(new_symbol);
137 return id2string(class_name) +
"::clinit_already_run";
229 const bool replace_clinit,
237 const auto base_name = base.
type().get_identifier();
239 if(
const auto base_init_func = symbol_table.
lookup(base_init_routine))
243 const irep_idt &clinit_name = replace_clinit
246 if(
const auto clinit_func = symbol_table.
lookup(clinit_name))
257 std::vector<irep_idt> nondet_ids;
261 [&](
const std::pair<irep_idt, symbolt> &symbol) {
263 declaring_class(symbol.second) == class_name &&
264 symbol.second.is_static_lifetime &&
265 !symbol.second.type.get_bool(ID_C_constant))
267 nondet_ids.push_back(symbol.first);
271 for(
const auto &
id : nondet_ids)
276 parameters.min_null_tree_depth =
289 pointer_type_selector,
332 function_symbol.
name = function_name;
334 function_symbol.
base_name = function_base_name;
335 function_symbol.
type = function_type;
339 function_symbol.
mode = ID_java;
340 bool failed = symbol_table.
add(function_symbol);
344 synthetic_methods.emplace(function_symbol.
name, synthetic_method_type);
346 insert_result.second,
347 "synthetic methods map should not already contain entry for " +
375 "user_specified_clinit",
395 const bool thread_safe)
436 class_name, symbol_table, synthetic_methods);
520 const bool replace_clinit,
527 INVARIANT(class_name,
"Wrapper function should have an owning class.");
529 const symbolt &clinit_state_sym =
531 const symbolt &clinit_thread_local_state_sym =
546 codet atomic_begin(ID_atomic_begin);
547 codet atomic_end(ID_atomic_end);
565 "Automatically generated function. States are:\n"
566 " 0 = class not initialized, init val of clinit_state/clinit_local_state\n"
567 " 1 = class initialization in progress, by this or another thread\n"
568 " 2 = initialization finished with success, by this or another thread\n";
577 function_body.
add(decl);
587 function_body.
add(std::move(conditional));
595 function_body.
add(assign);
600 function_body.
add(atomic_begin);
609 function_body.
add(assume);
634 std::move(init_conditional));
636 function_body.
add(std::move(not_init_conditional));
641 function_body.
add(atomic_end);
647 function_body.
add(std::move(conditional));
674 object_factory_parameters,
675 pointer_type_selector,
677 function_body.
append(init_body);
686 function_body.
add(atomic_begin);
690 function_body.
add(atomic_end);
694 return function_body;
716 const bool replace_clinit,
743 INVARIANT(class_name,
"Wrapper function should have an owning class.");
745 const symbolt &already_run_symbol =
762 object_factory_parameters,
763 pointer_type_selector,
767 return code_ifthenelset(std::move(check_already_run), std::move(init_body));
771 std::unordered_multimap<irep_idt, symbolt>
774 std::unordered_multimap<irep_idt, symbolt> result;
775 for(
const auto &symbol_pair : symbol_table)
777 const symbolt &symbol = symbol_pair.second;
779 result.emplace(*declaring, symbol);
789 size_t max_user_array_length,
790 std::unordered_map<std::string, object_creation_referencet> &references,
791 const std::unordered_multimap<irep_idt, symbolt>
792 &class_to_declared_symbols_map)
795 const auto clinit_func = symbol_table.
lookup(real_clinit_name);
796 if(clinit_func ==
nullptr)
803 const auto class_entry =
805 if(class_entry != static_values_json.
end() && class_entry->second.is_object())
807 const auto &class_json_object =
to_json_object(class_entry->second);
808 std::map<symbol_exprt, jsont> static_field_values;
809 for(
const auto &symbol_pair :
810 equal_range(class_to_declared_symbols_map, class_id))
812 const symbolt &symbol = symbol_pair.second;
816 const auto &static_field_entry =
818 if(static_field_entry != class_json_object.end())
820 static_field_values.insert(
821 {static_field_expr, static_field_entry->second});
826 for(
const auto &value_pair : static_field_values)
834 max_user_array_length,
839 auto it = references.find(reference_id);
840 INVARIANT(it != references.end(),
"reference id must be present in map");
844 for(
const auto &code_with_ref : code_with_references.
list)
845 body.
append(code_with_ref->to_code(reference_substitution));
870 const bool thread_safe,
871 const bool is_user_clinit_needed)
878 std::list<class_hierarchy_grapht::node_indext> topsorted_nodes =
881 for(
const auto node : topsorted_nodes)
883 const irep_idt &class_identifier = class_graph[node].class_identifier;
887 class_identifier, symbol_table, synthetic_methods, thread_safe);
888 if(is_user_clinit_needed)
891 class_identifier, symbol_table, synthetic_methods);
900 template<
class itertype>
904 auto initial_key = in->first;
905 while(in != end && in->first == initial_key)
920 const std::unordered_set<irep_idt> &stub_globals_set,
924 for(
const irep_idt &stub_global : stub_globals_set)
939 INVARIANT(class_id,
"Static field should have a defining class.");
954 "only stub classes should be given synthetic static initialisers");
957 "a class cannot be both incomplete, and so have stub static fields, and "
958 "also define a static initializer");
963 static_init_symbol.
name = static_init_name;
964 static_init_symbol.pretty_name = static_init_name;
965 static_init_symbol.base_name =
"clinit():V";
966 static_init_symbol.mode = ID_java;
967 static_init_symbol.type = thunk_type;
972 bool failed = symbol_table.
add(static_init_symbol);
975 auto insert_result = synthetic_methods.emplace(
976 static_init_symbol.name,
979 insert_result.second,
980 "synthetic methods map should not already contain entry for "
981 "stub static initializer");
1009 class_id,
"Synthetic static initializer should have an owning class.");
1018 !class_globals.empty(),
1019 "class with synthetic clinit should have at least one global to init");
1024 for(
const auto &pair : class_globals)
1044 pointer_type_selector,
1049 return static_init_body;
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
@ STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
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.
static void create_clinit_wrapper_function_symbol(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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...
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...
void set_function(const irep_idt &function)
synthetic_method_typet
Synthetic method kinds.
void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
Sets the identifier of the class which declared a given symbol to declaring_class.
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
The type of an expression, extends irept.
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
typet type
Type of symbol.
static void create_user_specified_clinit_function_symbol(const irep_idt &class_name, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
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.
iterator find(const std::string &key)
optionalt< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
const irept & find(const irep_namet &name) const
const std::string user_specified_clinit_suffix
A codet representing the declaration of a local variable.
bool is_clinit_function(const irep_idt &function_id)
Check if function_id is a clinit.
irep_idt user_specified_clinit_name(const irep_idt &class_name)
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
void create_static_initializer_symbols(symbol_tablet &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...
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.
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
Expression to hold a symbol (variable)
const std::string clinit_function_suffix
static irep_idt clinit_function_name(const irep_idt &class_name)
Get name of the real static initializer for a given class.
bool has_suffix(const std::string &s, const std::string &suffix)
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_tablet &symbol_table)
static void create_function_symbol(const irep_idt &class_name, const irep_idt &function_name, const irep_idt &function_base_name, const synthetic_method_typet &synthetic_method_type, symbol_tablet &symbol_table, synthetic_methods_mapt &synthetic_methods)
codet representation of an if-then-else statement.
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
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.
irep_idt pretty_name
Language-specific display name.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
void set_line(const irep_idt &line)
code_blockt get_user_specified_clinit_body(const irep_idt &class_id, const json_objectt &static_values_json, symbol_table_baset &symbol_table, optionalt< 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...
codet representation of a function call statement.
irep_idt mode
Language mode.
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
@ USER_SPECIFIED_STATIC_INITIALIZER
Only exists if the --static-values option was used.
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 std::string & id2string(const irep_idt &d)
static bool failed(bool error_indicator)
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 bool replace_clinit, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Generates codet that iterates through the base types of the class specified by class_name,...
#define PRECONDITION(CONDITION)
The symbol table base class interface.
static typet clinit_states_type()
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.
An assumption, which must hold in subsequent code.
void set_file(const irep_idt &file)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
const basest & bases() const
Get the collection of base classes/structs.
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.
static itertype advance_to_next_key(itertype in, itertype end)
Advance map iterator to next distinct key.
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
Information to store when several references point to the same Java object.
void add(const codet &code)
The Boolean constant false.
nonstd::optional< T > optionalt
size_t min_null_tree_depth
To force a certain depth of non-null objects.
signedbv_typet java_byte_type()
void append(code_with_references_listt &&other)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool is_user_specified_clinit_function(const irep_idt &function_id)
Check if function_id is a user-specified clinit.
exprt value
Initial value of symbol.
@ STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.
const std::string clinit_wrapper_suffix
codet representation of a "return from a function" statement.
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
json_objectt & to_json_object(jsont &json)
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
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.
clinit_statest
The three states in which a <clinit> method for a class can be before, after, and during static class...
std::list< std::shared_ptr< code_with_referencest > > list
void set(const irep_namet &name, const irep_idt &value)
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
stub_globals_by_classt stub_globals_by_class
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...
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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...
const java_class_typet & to_java_class_type(const typet &type)
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.
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...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
source_locationt & add_source_location()
empty_typet java_void_type()
A codet representing an assignment in the program.
The Boolean constant true.
A constant literal expression.
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.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
API to expression classes.
bool is_clinit_wrapper_function(const irep_idt &function_id)
Check if function_id is a clinit wrapper.
code_with_references_listt assign_from_json(const exprt &expr, const jsont &json, const irep_idt &function_id, symbol_table_baset &symbol_table, optionalt< ci_lazy_methods_neededt > &needed_lazy_methods, size_t max_user_array_length, std::unordered_map< std::string, object_creation_referencet > &references)
Given an expression expr representing a Java object or primitive and a JSON representation json of th...
irep_idt name
The unique identifier.
Base class or struct that a class or struct inherits from.
Data structure for representing an arbitrary statement in a program.
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
void populate(const symbol_tablet &)
Populate the class hierarchy graph, such that there is a node for every struct type in the symbol tab...