Pass information to clinit_wrapper constructors

Pass parameters necessary to nondet-initialize variables

Author: svorenova

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1035,9 +1035,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

@@ -186,7 +186,10 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 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())
@@ -384,7 +387,10 @@ static void create_clinit_wrapper_symbols(
 /// \return the body of the static initialiser 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);
@@ -535,7 +541,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);
   }
 
@@ -564,7 +576,10 @@ codet get_thread_safe_clinit_wrapper_body(
 /// \return the body of the static initialiser 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
@@ -608,7 +623,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
 {