Make get_user_specified_clinit_body take jsont arg

This avoids reparsing the whole json file for each class that needs a clinit.
Locally, on an example with a large json provided for --static-values,
execution time went from 10s to 2s.

Author: romainbrenguier

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -200,7 +200,13 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
     java_cp_include_files=".*";
 
   nondet_static = options.get_bool_option("nondet-static");
-  static_values_file = options.get_option("static-values");
+  if(options.is_set("static-values"))
+  {
+    const std::string filename = options.get_option("static-values");
+    jsont tmp_json;
+    if(!parse_json(filename, *message_handler, tmp_json))
+      static_values_json = std::move(tmp_json);
+  }
 
   if(options.is_set("context-include") || options.is_set("context-exclude"))
     method_in_context = get_context(options);
@@ -847,7 +853,7 @@ bool java_bytecode_languaget::typecheck(
     symbol_table,
     synthetic_methods,
     threading_support,
-    !static_values_file.empty());
+    static_values_json.has_value());
 
   // Now incrementally elaborate methods
   // that are reachable from this entry point.
@@ -1171,7 +1177,7 @@ bool java_bytecode_languaget::convert_single_method(
           function_id,
           symbol_table,
           nondet_static,
-          !static_values_file.empty(),
+          static_values_json.has_value(),
           object_factory_parameters,
           get_pointer_type_selector(),
           get_message_handler());
@@ -1180,7 +1186,7 @@ bool java_bytecode_languaget::convert_single_method(
           function_id,
           symbol_table,
           nondet_static,
-          !static_values_file.empty(),
+          static_values_json.has_value(),
           object_factory_parameters,
           get_pointer_type_selector(),
           get_message_handler());
@@ -1193,7 +1199,7 @@ bool java_bytecode_languaget::convert_single_method(
         class_name, "user_specified_clinit must be declared by a class.");
       writable_symbol.value = get_user_specified_clinit_body(
         *class_name,
-        static_values_file,
+        static_values_json,
         symbol_table,
         get_message_handler(),
         needed_lazy_methods,

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -229,10 +229,10 @@ class java_bytecode_languaget:public languaget
   java_string_library_preprocesst string_preprocess;
   std::string java_cp_include_files;
   bool nondet_static;
-  /// Path to a JSON file which contains initial values of static fields (right
+  /// JSON which contains initial values of static fields (right
   /// after the static initializer of the class was run). This is read from the
   /// --static-values command-line option.
-  std::string static_values_file;
+  optionalt<jsont> static_values_json;
 
   // list of classes to force load even without reference from the entry point
   std::vector<irep_idt> java_load_classes;

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -769,20 +769,17 @@ code_ifthenelset get_clinit_wrapper_body(
 
 code_blockt get_user_specified_clinit_body(
   const irep_idt &class_id,
-  const std::string &static_values_file,
+  const optionalt<jsont> &static_values_json,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   size_t max_user_array_length,
   std::unordered_map<std::string, object_creation_referencet> &references)
 {
-  jsont json;
   const irep_idt &real_clinit_name = clinit_function_name(class_id);
-  if(
-    !static_values_file.empty() &&
-    !parse_json(static_values_file, message_handler, json) && json.is_object())
+  if(static_values_json.has_value() && static_values_json->is_object())
   {
-    const auto &json_object = to_json_object(json);
+    const auto &json_object = to_json_object(*static_values_json);
     const auto class_entry =
       json_object.find(id2string(strip_java_namespace_prefix(class_id)));
     if(class_entry != json_object.end())

jbmc/src/java_bytecode/java_static_initializers.h

@@ -62,10 +62,9 @@ code_ifthenelset get_clinit_wrapper_body(
 /// 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.
+/// \param static_values_json: JSON object 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.
+///   values are maps from static field names to values.
 /// \param symbol_table: used to look up and create new symbols
 /// \param message_handler: used to log any errors with parsing the input file
 /// \param needed_lazy_methods: used to mark any runtime types given in the
@@ -77,7 +76,7 @@ code_ifthenelset get_clinit_wrapper_body(
 /// \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,
+  const optionalt<jsont> &static_values_json,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,