Create json_clinit symbol if --static-values is given

This function symbol is created in the same way as the one for
clinit_wrapper.
In this commit, the function has an empty body. It will be given content
in the following commits.

Author: antlechner

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -788,11 +788,11 @@ bool java_bytecode_languaget::typecheck(
       symbol_table, symbol_table_journal.get_inserted(), synthetic_methods);
   }
 
-  // For each class that will require a static initializer wrapper, create a
-  // function named package.classname::clinit_wrapper, and a corresponding
-  // global tracking whether it has run or not:
-  create_static_initializer_wrappers(
-    symbol_table, synthetic_methods, threading_support);
+  create_static_initializer_symbols(
+    symbol_table,
+    synthetic_methods,
+    threading_support,
+    !static_values_file.empty());
 
   // Now incrementally elaborate methods
   // that are reachable from this entry point.
@@ -1102,6 +1102,8 @@ bool java_bytecode_languaget::convert_single_method(
           get_pointer_type_selector(),
           get_message_handler());
       break;
+    case synthetic_method_typet::JSON_STATIC_INITIALIZER:
+      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

@@ -52,6 +52,7 @@ static typet clinit_states_type()
 // Disable linter here to allow a std::string constant, since that holds
 // a length, whereas a cstr would require strlen every time.
 const std::string clinit_wrapper_suffix = "::clinit_wrapper"; // NOLINT(*)
+const std::string json_clinit_suffix = "::json_clinit"; // NOLINT(*)
 const std::string clinit_function_suffix = ".<clinit>:()V"; // NOLINT(*)
 
 /// Get the Java static initializer wrapper name for a given class (the wrapper
@@ -65,6 +66,11 @@ irep_idt clinit_wrapper_name(const irep_idt &class_name)
   return id2string(class_name) + clinit_wrapper_suffix;
 }
 
+irep_idt json_clinit_name(const irep_idt &class_name)
+{
+  return id2string(class_name) + json_clinit_suffix;
+}
+
 /// Check if function_id is a clinit wrapper
 /// \param function_id: some function identifier
 /// \return true if the passed identifier is a clinit wrapper
@@ -335,6 +341,21 @@ static void create_clinit_wrapper_function_symbol(
     synthetic_methods);
 }
 
+// Create symbol for the "json_clinit"
+static void create_json_clinit_function_symbol(
+  const irep_idt &class_name,
+  symbol_tablet &symbol_table,
+  synthetic_methods_mapt &synthetic_methods)
+{
+  create_function_symbol(
+    class_name,
+    json_clinit_name(class_name),
+    "json_clinit",
+    synthetic_method_typet::JSON_STATIC_INITIALIZER,
+    symbol_table,
+    synthetic_methods);
+}
+
 /// Creates a static initializer wrapper symbol for the given class, along with
 /// a global boolean that tracks if it has been run already.
 /// \param class_name: class symbol name
@@ -716,17 +737,27 @@ code_ifthenelset get_clinit_wrapper_body(
   return code_ifthenelset(std::move(check_already_run), std::move(init_body));
 }
 
-/// Create static initializer wrappers for all classes that need them.
+/// 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
+/// function named package.classname::clinit_wrapper, and a corresponding
+/// global tracking whether it has run or not. If a JSON file containing static
+/// values is given, also create a function named
+/// package.classname::json_clinit.
 /// \param symbol_table: global symbol table
 /// \param synthetic_methods: synthetic methods map. Will be extended noting
 ///   that any wrapper belongs to this code, and so `get_clinit_wrapper_body`
 ///   should be used to produce the method body when required.
 /// \param thread_safe: if true state variables required to make the
 ///   clinit_wrapper thread safe will be created.
-void create_static_initializer_wrappers(
+/// \param is_json_clinit_needed: determines whether or not a symbol for the
+///   synthetic json_clinit function should be created. This is true if a file
+///   was given with the --static-values option and false otherwise.
+void create_static_initializer_symbols(
   symbol_tablet &symbol_table,
   synthetic_methods_mapt &synthetic_methods,
-  const bool thread_safe)
+  const bool thread_safe,
+  const bool is_json_clinit_needed)
 {
   // Top-sort the class hierarchy, such that we visit parents before children,
   // and can so identify parents that need static initialisation by whether we
@@ -743,6 +774,11 @@ void create_static_initializer_wrappers(
     {
       create_clinit_wrapper_symbols(
         class_identifier, symbol_table, synthetic_methods, thread_safe);
+      if(is_json_clinit_needed)
+      {
+        create_json_clinit_function_symbol(
+          class_identifier, symbol_table, synthetic_methods);
+      }
     }
   }
 }

jbmc/src/java_bytecode/java_static_initializers.h

@@ -20,13 +20,15 @@ Author: Chris Smowton, [email protected]
 #include <util/symbol_table.h>
 
 irep_idt clinit_wrapper_name(const irep_idt &class_name);
+irep_idt json_clinit_name(const irep_idt &class_name);
 
 bool is_clinit_wrapper_function(const irep_idt &function_id);
 
-void create_static_initializer_wrappers(
+void create_static_initializer_symbols(
   symbol_tablet &symbol_table,
   synthetic_methods_mapt &synthetic_methods,
-  const bool thread_safe);
+  const bool thread_safe,
+  const bool is_json_clinit_needed);
 
 code_blockt get_thread_safe_clinit_wrapper_body(
   const irep_idt &function_id,

jbmc/src/java_bytecode/synthetic_methods_map.h

@@ -27,6 +27,9 @@ enum class synthetic_method_typet
   /// These are generated for both user and stub types, to ensure the actual
   /// 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.
+  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
   /// generate a static initializer function to initialize its static fields.