1/*******************************************************************\
3Module: Java Static Initializers
5Author: Chris Smowton, chris.smowton@diffblue.com
7\*******************************************************************/
61// Disable linter here to allow a std::string constant, since that holds
62// a length, whereas a cstr would require strlen every time.
120 const bool is_thread_local,
121 const bool is_static_lifetime)
124 new_symbol.pretty_name = name;
125 new_symbol.base_name = name;
127 new_symbol.value = value;
128 new_symbol.is_lvalue =
true;
129 new_symbol.is_state_var =
true;
130 new_symbol.is_static_lifetime = is_static_lifetime;
131 new_symbol.is_thread_local = is_thread_local;
132 symbol_table.
add(new_symbol);
142 return id2string(class_name) +
"::clinit_already_run";
242 const auto base_name = base.type().get_identifier();
254 // If nondet-static option is given, add a standard nondet initialization for
255 // each non-final static field of this class. Note this is the same invocation
256 // used in get_stub_initializer_body and java_static_lifetime_init.
266 [&](
const std::pair<irep_idt, symbolt> &symbol) {
268 declaring_class(symbol.second) == class_name &&
269 symbol.second.is_static_lifetime &&
270 !symbol.second.type.get_bool(ID_C_constant))
272 nondet_ids.push_back(symbol.first);
281 parameters.min_null_tree_depth =
294 pointer_type_selector,
341 // This provides a back-link from a method to its associated class, as is done
342 // for java_bytecode_convert_methodt::convert.
351 "synthetic methods map should not already contain entry for " +
355// Create symbol for the "clinit_wrapper"
370// Create symbol for the "user_specified_clinit"
379 "user_specified_clinit",
406 // Create two global static synthetic "fields" for the class "id"
407 // these two variables hold the state of the class initialization algorithm
408 // across calls to the clinit_wrapper
440 class_name, symbol_table, synthetic_methods);
531 INVARIANT(class_name,
"Wrapper function should have an owning class.");
538 // Create a function-local variable "init_complete". This variable is used to
539 // avoid inspecting the global state (clinit_state_sym) outside of
540 // the critical-section.
554 // This code defines source locations for every codet generated below for
555 // the static initializer wrapper. Enable this for debugging the symex going
556 // through the clinit_wrapper.
558 // java::C.<clinit_wrapper>()
559 // You will additionally need to associate the `location` with the
560 // `function_body` and then manually set lines of code for each of the
561 // statements of the function, using something along the lines of:
562 // `mycodet.then_case().add_source_location().set_line(17);`/
569 "Automatically generated function. States are:\n"
570 " 0 = class not initialized, init val of clinit_state/clinit_local_state\n"
571 " 1 = class initialization in progress, by this or another thread\n"
572 " 2 = initialization finished with success, by this or another thread\n";
578 // bool init_complete;
584 // if(C::__CPROVER_PREFIX_clinit_thread_local_state == INIT_COMPLETE) return;
594 // C::__CPROVER_PREFIX_clinit_thread_local_state = INIT_COMPLETE;
607 // Assume: clinit_state_sym != IN_PROGRESS
616 // If(C::__CPROVER_PREFIX_clinit_state == NOT_INIT)
618 // C::__CPROVER_PREFIX_clinit_state = IN_PROGRESS;
619 // init_complete = false;
621 // else If(C::__CPROVER_PREFIX_clinit_state == INIT_COMPLETE)
623 // init_complete = true;
649 // if(init_complete) return;
656 // Initialize the super-class C' and
657 // the implemented interfaces l_1 ... l_n.
658 // see JVMS p.359 step 7, for the exact definition of
659 // the sequence l_1 to l_n.
660 // This is achieved by iterating through the base types and
661 // adding recursive calls to the clinit_wrapper()
663 // java::C'.<clinit_wrapper>();
664 // java::I1.<clinit_wrapper>();
665 // java::I2.<clinit_wrapper>();
667 // java::In.<clinit_wrapper>();
669 // java::C.<clinit>(); // or nondet-initialization of all static
670 // // variables of C if nondet-static is true
680 object_factory_parameters,
681 pointer_type_selector,
687 // C::__CPROVER_PREFIX_clinit_state = INIT_COMPLETE;
691 // synchronization prologue
727 // Assume that class C extends class C' and implements interfaces
728 // I1, ..., In. We now create the following function (possibly recursively
729 // creating the clinit_wrapper functions for C' and I1, ..., In):
731 // java::C.<clinit_wrapper>()
733 // if (!java::C::clinit_already_run)
735 // java::C::clinit_already_run = true; // before recursive calls!
737 // java::C'.<clinit_wrapper>();
738 // java::I1.<clinit_wrapper>();
739 // java::I2.<clinit_wrapper>();
741 // java::In.<clinit_wrapper>();
743 // java::C.<clinit>(); // or nondet-initialization of all static
744 // // variables of C if nondet-static is true
749 INVARIANT(class_name,
"Wrapper function should have an owning class.");
758 // add the "already-run = false" statement
769 object_factory_parameters,
770 pointer_type_selector,
773 // the entire body of the function is an if-then-else
778std::unordered_multimap<irep_idt, symbolt>
781 std::unordered_multimap<irep_idt, symbolt> result;
795 std::optional<ci_lazy_methods_neededt> needed_lazy_methods,
796 size_t max_user_array_length,
797 std::unordered_map<std::string, object_creation_referencet> &references,
798 const std::unordered_multimap<irep_idt, symbolt>
805 // Case where the real clinit doesn't appear in the symbol table, even
806 // though their is user specifed one. This may occur when some class
807 // substitution happened after compilation.
841 max_user_array_length,
846 auto it = references.find(reference_id);
847 INVARIANT(it != references.end(),
"reference id must be present in map");
880 // Top-sort the class hierarchy, such that we visit parents before children,
881 // and can so identify parents that need static initialisation by whether we
882 // have made them a clinit_wrapper method.
894 class_identifier, symbol_table, synthetic_methods,
thread_safe);
898 class_identifier, symbol_table, synthetic_methods);
907template<
class itertype>
930 // Populate map from class id -> stub globals:
936 // This symbol is already nondet-initialised during __CPROVER_initialize
937 // (generated in java_static_lifetime_init). In future this will only
938 // be the case for primitive-typed fields, but for now reference-typed
939 // fields can also be treated this way in the exceptional case that they
940 // belong to a non-stub class. Skip the field, as it does not need a
941 // synthetic static initializer.
946 INVARIANT(class_id,
"Static field should have a defining class.");
950 // For each distinct class that has stub globals, create a clinit symbol:
961 "only stub classes should be given synthetic static initialisers");
964 "a class cannot be both incomplete, and so have stub static fields, and "
965 "also define a static initializer");
971 // This provides a back-link from a method to its associated class, as is
972 // done for java_bytecode_convert_methodt::convert.
983 "synthetic methods map should not already contain entry for "
984 "stub static initializer");
1012 class_id,
"Synthetic static initializer should have an owning class.");
1015 // Add a standard nondet initialisation for each global declared on this
1016 // class. Note this is the same invocation used in
1017 // java_static_lifetime_init.
1022 "class with synthetic clinit should have at least one global to init");
1047 pointer_type_selector,
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
code_with_references_listt assign_from_json(const exprt &expr, const jsont &json, const irep_idt &function_id, 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)
Given an expression expr representing a Java object or primitive and a JSON representation json of th...
Context-insensitive lazy methods container.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Class hierarchy, represented using grapht and therefore suitable for use with generic graph algorithm...
An assumption, which must hold in subsequent code.
A codet representing sequential composition of program statements.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
codet representation of a "return from a function" statement.
goto_instruction_codet representation of a function call statement.
codet representation of an if-then-else statement.
Wrapper around a list of shared pointer to code_with_referencest objects, which provides a nicer inte...
std::function< const object_creation_referencet &(const std::string &)> reference_substitutiont
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
The Boolean constant false.
iterator find(const std::string &key)
void set_file(const irep_idt &file)
void set_line(const irep_idt &line)
void set_function(const irep_idt &function)
Base class or struct that a class or struct inherits from.
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...
stub_globals_by_classt stub_globals_by_class
Expression to hold a symbol (variable)
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
irep_idt irep_idt base_name
Name of module the symbol belongs to.
The Boolean constant true.
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
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...
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
std::unordered_multimap< irep_idt, symbolt > class_to_declared_symbols(const symbol_table_baset &symbol_table)
static code_frontend_assignt gen_clinit_assign(const exprt &expr, const clinit_statest state)
Generates a code_frontend_assignt for clinit_statest /param expr: expression to be used as the LHS of...
clinit_statest
The three states in which a <clinit> method for a class can be before, after, and during static class...
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...
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_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods)
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...
static typet clinit_states_type()
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 clinit_function_suffix
static void create_user_specified_clinit_function_symbol(const irep_idt &class_name, symbol_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods)
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_table_baset &symbol_table, synthetic_methods_mapt &synthetic_methods)
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...
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,...
static void create_clinit_wrapper_symbols(const irep_idt &class_name, symbol_table_baset &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...
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)
const std::string user_specified_clinit_suffix
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.
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 itertype advance_to_next_key(itertype in, itertype end)
Advance map iterator to next distinct key.
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...
static irep_idt clinit_function_name(const irep_idt &class_name)
Get name of the real static initializer for a given class.
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.
bool is_clinit_function(const irep_idt &function_id)
Check if function_id is a clinit.
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.
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.
const std::string clinit_wrapper_suffix
static bool needs_clinit_wrapper(const irep_idt &class_name, const symbol_table_baset &symbol_table)
Checks whether a static initializer wrapper is needed for a given class, i.e.
empty_typet java_void_type()
signedbv_typet java_byte_type()
const java_class_typet & to_java_class_type(const typet &type)
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
std::optional< irep_idt > declaring_class(const symbolt &symbol)
Gets the identifier of the class which declared a given symbol.
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.
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
json_objectt & to_json_object(jsont &json)
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.
static std::string comment(const rw_set_baset::entryt &entry, bool write)
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.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Information to store when several references point to the same Java object.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
size_t min_null_tree_depth
To force a certain depth of non-null objects.
bool has_suffix(const std::string &s, const std::string &suffix)
static bool failed(bool error_indicator)
std::unordered_map< irep_idt, synthetic_method_typet > synthetic_methods_mapt
Maps method names on to a synthetic method kind.
synthetic_method_typet
Synthetic method kinds.
@ USER_SPECIFIED_STATIC_INITIALIZER
Only exists if the --static-values option was used.
@ STATIC_INITIALIZER_WRAPPER
A static initializer wrapper (code of the form if(!already_run) clinit(); already_run = true;) These ...
@ STUB_CLASS_STATIC_INITIALIZER
A generated (synthetic) static initializer function for a stub type.