Set up structure of function for json_clinit body

To get the assignments from the JSON file, we will have to
- parse the JSON file
- look up the given class name in the JSON file
- for each static field of this class in the symbol table, look up the
field name in the class entry of the JSON 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

@@ -1102,6 +1102,11 @@ bool java_bytecode_languaget::convert_single_method(
           get_message_handler());
       break;
     case synthetic_method_typet::JSON_STATIC_INITIALIZER:
+      writable_symbol.value = get_json_clinit_body(
+        function_id,
+        static_values_file,
+        symbol_table,
+        get_message_handler());
       break;
     case synthetic_method_typet::STUB_CLASS_STATIC_INITIALIZER:
       writable_symbol.value =

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
@@ -744,6 +745,60 @@ code_ifthenelset get_clinit_wrapper_body(
   return code_ifthenelset(std::move(check_already_run), std::move(init_body));
 }
 
+code_blockt get_json_clinit_body(
+  const irep_idt &function_id,
+  const std::string &static_values_file,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
+{
+  const auto class_name = declaring_class(symbol_table.lookup_ref(function_id));
+  INVARIANT(class_name, "json_clinit must be declared by a class.");
+  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_name)));
+    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) == class_name && 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
+        }
+        return body;
+      }
+    }
+  }
+  const irep_idt &real_clinit_name = clinit_function_name(*class_name);
+  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 assignments from a JSON file
 /// 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,31 @@ code_ifthenelset get_clinit_wrapper_body(
   const select_pointer_typet &pointer_type_selector,
   message_handlert &message_handler);
 
+/// Creates the body of a json_clinit function, which includes assignments for
+/// all static fields of a class to values read from a JSON file. If the JSON
+/// file could not be parsed or an entry for this class could not be found in
+/// the JSON file, the function will only include 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 JSON file,
+/// those fields will be assigned default values.
+/// \param function_id: the id of this json_clinit function
+/// \param static_values_file: JSON 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.
+/// \param symbol_table: used to look up and create new symbols
+/// \param message_handler: used log any errors with parsing the JSON
+/// \param needed_lazy_methods: used to mark any runtime types given in the JSON
+///   file as needed
+/// \param max_user_array_length: maximum value for constant or variable length
+///   arrays. Any arrays that were specified to be of nondeterministic length in
+///   the JSON file will be limited by this value.
+/// \param references:
+/// \return the body of the json_clinit function as a code block.
+code_blockt get_json_clinit_body(
+  const irep_idt &function_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,6 +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.
+  /// If a given type has an entry in the file given by this option, the JSON
+  /// JSON static initializer contains a sequence of assignments from static
+  /// field expressions to values read from the JSON file.
+  /// Otherwise, this function simply calls the regular clinit.
   JSON_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