Nondet-initialize variables in clinit_wrapper constructor

If nondet-static option is used

Author: svorenova

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -179,7 +179,8 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 
 /// Generates codet that iterates through the base types of the class specified
 /// by class_name, C, and recursively adds calls to their clinit wrapper.
-/// Finally a call to the clinint wrapper of C is made.
+/// Finally a call to the clinit of C is made or if nondet-static option was
+/// given then all static variables of the class are nondet-initialized instead.
 /// \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
@@ -190,7 +191,7 @@ gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 /// \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,
+  symbol_table_baset &symbol_table,
   const irep_idt &class_name,
   code_blockt &init_body,
   const bool nondet_static,
@@ -214,9 +215,48 @@ static void clinit_wrapper_do_recursive_calls(
   auto find_sym_it = symbol_table.symbols.find(real_clinit_name);
   if(find_sym_it != symbol_table.symbols.end())
   {
-    code_function_callt call_real_init;
-    call_real_init.function() = find_sym_it->second.symbol_expr();
-    init_body.move_to_operands(call_real_init);
+    if(!nondet_static)
+    {
+      code_function_callt call_real_init;
+      call_real_init.function() = find_sym_it->second.symbol_expr();
+      init_body.move_to_operands(call_real_init);
+    }
+    else
+    {
+      // Add a standard nondet initialisation for each global declared on this
+      // class. Note this is the same invocation used in
+      // get_stub_initializer_body and java_static_lifetime_init.
+
+      object_factory_parameterst parameters = object_factory_parameters;
+      parameters.function_id = real_clinit_name;
+
+      for(const auto &symbol : symbol_table.symbols)
+      {
+        if(
+          symbol.second.is_static_lifetime &&
+          symbol.second.type.get(ID_C_class) == class_name)
+        {
+          const symbol_exprt new_global_symbol = symbol.second.symbol_expr();
+
+          parameters.max_nonnull_tree_depth =
+            is_non_null_library_global(symbol.first)
+              ? std::max(
+                  size_t(1), object_factory_parameters.max_nonnull_tree_depth)
+              : object_factory_parameters.max_nonnull_tree_depth;
+
+          gen_nondet_init(
+            new_global_symbol,
+            init_body,
+            symbol_table,
+            source_locationt(),
+            false,
+            allocation_typet::DYNAMIC,
+            parameters,
+            pointer_type_selector,
+            update_in_placet::NO_UPDATE_IN_PLACE);
+        }
+      }
+    }
   }
 }
 
@@ -373,7 +413,8 @@ static void create_clinit_wrapper_symbols(
 ///   // ...
 ///   java::In::clinit_wrapper();
 ///
-///   java::C::<clinit>();
+///   java::C::<clinit>();  // or nondet-initialization of all static
+///                         // variables of C if nondet-static is true
 ///
 ///   // Setting this variable to INIT_COMPLETE will let other threads "cross"
 ///   // beyond the assume() statement above in this function.
@@ -549,7 +590,8 @@ codet get_thread_safe_clinit_wrapper_body(
   //  // ...
   //  java::In::clinit_wrapper();
   //
-  //  java::C::<clinit>();
+  //  java::C::<clinit>(); // or nondet-initialization of all static
+  //                       // variables of C if nondet-static is true
   //
   {
     code_blockt init_body;
@@ -615,7 +657,8 @@ codet get_clinit_wrapper_body(
   //     // ...
   //     java::In::clinit_wrapper();
   //
-  //     java::C::<clinit>();
+  //     java::C::<clinit>(); // or nondet-initialization of all static
+  //                          // variables of C if nondet-static is true
   //   }
   // }
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);