Set up structure of function creating user_specified_clinit body

To get the assignments from the input file, we will have to
- parse the file
- look up the given class name in the file
- for each static field of this class in the symbol table, look up the
  field name in the class entry of the file
- if an entry was found, the "TODO" is hit: in the following commits the
  actual assignments will be added here.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1106,7 +1106,15 @@ bool java_bytecode_languaget::convert_single_method(
           get_message_handler());
       break;
     case synthetic_method_typet::USER_SPECIFIED_STATIC_INITIALIZER:
+    {
+      const auto class_name =
+        declaring_class(symbol_table.lookup_ref(function_id));
+      INVARIANT(
+        class_name, "user_specified_clinit must be declared by a class.");
+      writable_symbol.value = get_user_specified_clinit_body(
+        *class_name, static_values_file, symbol_table, get_message_handler());
       break;
+    }
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       writable_symbol.value =
         stub_global_initializer_factory.get_stub_initializer_body(

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -10,11 +10,12 @@ Author: Chris Smowton, [email protected]
 #include "java_object_factory.h"
 #include "java_utils.h"
 #include <goto-programs/class_hierarchy.h>
-#include <util/std_types.h>
-#include <util/std_expr.h>
+#include <json/json_parser.h>
+#include <util/arith_tools.h>
 #include <util/std_code.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
 #include <util/suffix.h>
-#include <util/arith_tools.h>
 
 /// The three states in which a `<clinit>` method for a class can be before,
 /// after, and during static class initialization. These states are only used
@@ -750,6 +751,61 @@ code_ifthenelset get_clinit_wrapper_body(
   return code_ifthenelset(std::move(check_already_run), std::move(init_body));
 }
 
+code_blockt get_user_specified_clinit_body(
+  const irep_idt &class_id,
+  const std::string &static_values_file,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
+{
+  jsont json;
+  if(
+    !static_values_file.empty() &&
+    !parse_json(static_values_file, message_handler, json) && json.is_object())
+  {
+    const auto &json_object = to_json_object(json);
+    const auto class_entry =
+      json_object.find(id2string(strip_java_namespace_prefix(class_id)));
+    if(class_entry != json_object.end())
+    {
+      const auto &class_json_value = class_entry->second;
+      if(class_json_value.is_object())
+      {
+        const auto &class_json_object = to_json_object(class_json_value);
+        std::map<symbol_exprt, jsont> static_field_values;
+        for(const auto &symbol_pair : symbol_table)
+        {
+          const symbolt &symbol = symbol_pair.second;
+          if(
+            declaring_class(symbol) && *declaring_class(symbol) == class_id &&
+            symbol.is_static_lifetime)
+          {
+            const symbol_exprt &static_field_expr = symbol.symbol_expr();
+            const auto &static_field_entry =
+              class_json_object.find(id2string(symbol.base_name));
+            if(static_field_entry != class_json_object.end())
+            {
+              static_field_values.insert(
+                {static_field_expr, static_field_entry->second});
+            }
+          }
+        }
+        code_blockt body;
+        for(const auto &value_pair : static_field_values)
+        {
+          // TODO append code to `body` to assign value_pair.first to
+          // TODO value_pair.second
+          (void)value_pair;
+        }
+        return body;
+      }
+    }
+  }
+  const irep_idt &real_clinit_name = clinit_function_name(class_id);
+  if(const auto clinit_func = symbol_table.lookup(real_clinit_name))
+    return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};
+  return code_blockt{};
+}
+
 /// Create static initializer wrappers and possibly user-specified functions for
 /// initial static field value assignments for all classes that need them.
 /// For each class that will require a static initializer wrapper, create a

jbmc/src/java_bytecode/java_static_initializers.h

@@ -48,6 +48,29 @@ code_ifthenelset get_clinit_wrapper_body(
   const select_pointer_typet &pointer_type_selector,
   message_handlert &message_handler);
 
+/// Create the body of a user_specified_clinit function for a given class, which
+/// includes assignments for all static fields of the class to values read from
+/// an input file. If the file could not be parsed or an entry for this class
+/// could not be found in it, the user_specified_clinit function will only
+/// contain a call to the "real" clinit function, and not include any
+/// assignments itself. If an entry for this class is found but some of its
+/// static fields are not mentioned in the input file, those fields will be
+/// assigned default values (zero or null).
+/// \param class_id: the id of the class to create a user_specified_clinit
+///   function body for.
+/// \param static_values_file: input file containing values of static fields.
+///   The format is expected to be a map whose keys are class names, and whose
+///   values are maps from static field names to values. Currently only JSON
+///   is supported as a file format.
+/// \param symbol_table: used to look up and create new symbols
+/// \param message_handler: used to log any errors with parsing the input file
+/// \return the body of the user_specified_clinit function as a code block.
+code_blockt get_user_specified_clinit_body(
+  const irep_idt &class_id,
+  const std::string &static_values_file,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler);
+
 class stub_global_initializer_factoryt
 {
   /// Maps class symbols onto the stub globals that belong to them

jbmc/src/java_bytecode/synthetic_methods_map.h

@@ -28,7 +28,10 @@ enum class synthetic_method_typet
   /// static initializer is only run once on any given path.
   STATIC_INITIALIZER_WRAPPER,
   /// Only exists if the `--static-values` option was used.
-  /// TODO Currently has no content, future commits will add it.
+  /// If a given type has an entry in the file given by this option, the "user
+  /// specified static initializer" contains a sequence of assignments from
+  /// static field expressions to values read from the file.
+  /// Otherwise, this function simply calls the regular clinit.
   USER_SPECIFIED_STATIC_INITIALIZER,
   /// A generated (synthetic) static initializer function for a stub type.
   /// Because we don't have the bytecode for a stub type (by definition), we