Pass information to clinit_wrapper constructors

Pass parameters necessary to nondet-initialize variables

Author: svorenova

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1031,9 +1031,18 @@ bool java_bytecode_languaget::convert_single_method(
     case synthetic_method_typet::STATIC_INITIALIZER_WRAPPER:
       if(threading_support)
         symbol.value = get_thread_safe_clinit_wrapper_body(
-          function_id, symbol_table);
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       else
-        symbol.value = get_clinit_wrapper_body(function_id, symbol_table);
+        symbol.value = get_clinit_wrapper_body(
+          function_id,
+          symbol_table,
+          nondet_static,
+          object_factory_parameters,
+          get_pointer_type_selector());
       break;
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       symbol.value =

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -184,10 +184,19 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 /// \param symbol_table: symbol table
 /// \param class_name: name of the class to generate clinit wrapper calls for
 /// \param [out] init_body: appended with calls to clinit wrapper
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
 static void clinit_wrapper_do_recursive_calls(
   const symbol_tablet &symbol_table,
   const irep_idt &class_name,
-  code_blockt &init_body)
+  code_blockt &init_body,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
   for(const auto &base : to_class_type(class_symbol.type).bases())
@@ -316,9 +325,9 @@ static void create_clinit_wrapper_symbols(
     "clinit wrapper");
 }
 
-/// Thread safe version of the static initialiser.
+/// Thread safe version of the static initializer.
 ///
-/// Produces the static initialiser wrapper body for the given function. This
+/// Produces the static initializer wrapper body for the given function. This
 /// static initializer implements (a simplification of) the algorithm defined
 /// in Section 5.5 of the JVM Specs. This function, or wrapper, checks whether
 /// static init has already taken place, calls the actual `<clinit>` method if
@@ -382,10 +391,19 @@ static void create_clinit_wrapper_symbols(
 /// \param function_id: clinit wrapper function id (the wrapper_method_symbol
 ///   name created by `create_clinit_wrapper_symbols`)
 /// \param symbol_table: global symbol table
-/// \return the body of the static initialiser wrapper
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
+/// \return the body of the static initializer wrapper
 codet get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
   irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
@@ -536,7 +554,13 @@ codet get_thread_safe_clinit_wrapper_body(
   //
   {
     code_blockt init_body;
-    clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
+    clinit_wrapper_do_recursive_calls(
+      symbol_table,
+      class_name,
+      init_body,
+      nondet_static,
+      object_factory_parameters,
+      pointer_type_selector);
     function_body.append(init_body);
   }
 
@@ -557,15 +581,24 @@ codet get_thread_safe_clinit_wrapper_body(
   return function_body;
 }
 
-/// Produces the static initialiser wrapper body for the given function.
+/// Produces the static initializer wrapper body for the given function.
 /// Note: this version of the clinit wrapper is not thread safe.
 /// \param function_id: clinit wrapper function id (the wrapper_method_symbol
 ///   name created by `create_clinit_wrapper_symbols`)
 /// \param symbol_table: global symbol table
-/// \return the body of the static initialiser wrapper/
+/// \param nondet_static: true if nondet-static option was given
+/// \param object_factory_parameters: object factory parameters used to populate
+///   nondet-initialized globals and objects reachable from them (only needed
+///   if nondet-static is true)
+/// \param pointer_type_selector: used to choose concrete types for abstract-
+///   typed globals and fields (only needed if nondet-static is true)
+/// \return the body of the static initializer wrapper
 codet get_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table)
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector)
 {
   // Assume that class C extends class C' and implements interfaces
   // I1, ..., In. We now create the following function (possibly recursively
@@ -609,7 +642,13 @@ codet get_clinit_wrapper_body(
   code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt());
   init_body.move_to_operands(set_already_run);
 
-  clinit_wrapper_do_recursive_calls(symbol_table, class_name, init_body);
+  clinit_wrapper_do_recursive_calls(
+    symbol_table,
+    class_name,
+    init_body,
+    nondet_static,
+    object_factory_parameters,
+    pointer_type_selector);
 
   wrapper_body.then_case() = init_body;
 

jbmc/src/java_bytecode/java_static_initializers.h

@@ -29,11 +29,17 @@ void create_static_initializer_wrappers(
 
 codet get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector);
 
 codet get_clinit_wrapper_body(
   const irep_idt &function_id,
-  symbol_table_baset &symbol_table);
+  symbol_table_baset &symbol_table,
+  const bool nondet_static,
+  const object_factory_parameterst &object_factory_parameters,
+  const select_pointer_typet &pointer_type_selector);
 
 class stub_global_initializer_factoryt
 {