[TG-9299] Fix crash in case of user provided clinit for a clinit which is not in the symbol table

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -838,7 +838,9 @@ void assign_from_json(
   location.set_function(function_id);
   allocate_objectst allocate(ID_java, location, function_id, symbol_table);
   code_blockt body_rec;
-  const auto class_name = declaring_class(symbol_table.lookup_ref(function_id));
+  const symbolt *function_symbol = symbol_table.lookup(function_id);
+  INVARIANT(function_symbol, "Function must appear in symbol table");
+  const auto class_name = declaring_class(*function_symbol);
   INVARIANT(
     class_name,
     "Function " + id2string(function_id) + " must be declared by a class.");

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -792,50 +792,52 @@ code_blockt get_user_specified_clinit_body(
     &class_to_declared_symbols_map)
 {
   const irep_idt &real_clinit_name = clinit_function_name(class_id);
+  const auto clinit_func = symbol_table.lookup(real_clinit_name);
+  if(clinit_func == nullptr)
+  {
+    // Case where the real clinit doesn't appear in the symbol table, even
+    // though their is user specifed one. This may occur when some class
+    // substitution happened after compilation.
+    return code_blockt{};
+  }
   const auto class_entry =
     static_values_json.find(id2string(strip_java_namespace_prefix(class_id)));
-  if(class_entry != static_values_json.end())
+  if(class_entry != static_values_json.end() && class_entry->second.is_object())
   {
-    const auto &class_json_value = class_entry->second;
-    if(class_json_value.is_object())
+    const auto &class_json_object = to_json_object(class_entry->second);
+    std::map<symbol_exprt, jsont> static_field_values;
+    for(const auto &symbol_pair :
+        equal_range(class_to_declared_symbols_map, class_id))
     {
-      const auto &class_json_object = to_json_object(class_json_value);
-      std::map<symbol_exprt, jsont> static_field_values;
-      for(const auto &class_symbol_pair :
-          equal_range(class_to_declared_symbols_map, class_id))
+      const symbolt &symbol = symbol_pair.second;
+      if(symbol.is_static_lifetime)
       {
-        const symbolt &symbol = class_symbol_pair.second;
-        if(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())
         {
-          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});
-          }
+          static_field_values.insert(
+            {static_field_expr, static_field_entry->second});
         }
       }
-      code_blockt body;
-      for(const auto &value_pair : static_field_values)
-      {
-        assign_from_json(
-          value_pair.first,
-          value_pair.second,
-          real_clinit_name,
-          body,
-          symbol_table,
-          needed_lazy_methods,
-          max_user_array_length,
-          references);
-      }
-      return body;
     }
+    code_blockt body;
+    for(const auto &value_pair : static_field_values)
+    {
+      assign_from_json(
+        value_pair.first,
+        value_pair.second,
+        real_clinit_name,
+        body,
+        symbol_table,
+        needed_lazy_methods,
+        max_user_array_length,
+        references);
+    }
+    return body;
   }
-  if(const auto clinit_func = symbol_table.lookup(real_clinit_name))
-    return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};
-  return code_blockt{};
+  return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};
 }
 
 /// Create static initializer wrappers and possibly user-specified functions for

jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp

@@ -108,6 +108,30 @@ SCENARIO("get_user_specified_clinit_body", "[core][java_static_initializers]")
       REQUIRE(clinit_body == code_blockt{});
     }
   }
+  GIVEN(
+    "A class which has an entry in the JSON object but no clinit defined "
+    "in the symbol table")
+  {
+    static_values_json["TestClass"] = [] {
+      json_objectt entry{};
+      entry["field_name"] = json_numbert{"42"};
+      return entry;
+    }();
+
+    const code_blockt clinit_body = get_user_specified_clinit_body(
+      "java::TestClass",
+      static_values_json,
+      symbol_table,
+      {},
+      max_user_array_length,
+      references,
+      class_to_declared_symbols);
+
+    THEN("User provided clinit body is empty")
+    {
+      REQUIRE(clinit_body == code_blockt{});
+    }
+  }
   GIVEN("A class which has a static number in the provided JSON")
   {
     static_values_json["TestClass"] = [] {