assign_from_json returns code_with_references_listt

This will allow references to be replaced after the all value pairs
have been replaced.
For instance in the regression test
regression/jbmc/deterministic_assignments_json/test_char_array_pass.desc
the reference 2 wouldn't have been assigned before the end of the
assign_from_json call in which it is referenced for the first time so
its allocation size would be non-deterministic but this is fixed by this
commit.

Author: romainbrenguier

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -902,11 +902,10 @@ code_with_references_listt assign_from_json_rec(
   return result;
 }
 
-void assign_from_json(
+code_with_references_listt assign_from_json(
   const exprt &expr,
   const jsont &json,
   const irep_idt &function_id,
-  code_blockt &assignments,
   symbol_table_baset &symbol_table,
   optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
   size_t max_user_array_length,
@@ -930,15 +929,15 @@ void assign_from_json(
                              location,
                              max_user_array_length,
                              class_type};
-  code_blockt body;
-  code_with_referencest::reference_substitutiont reference_substitution =
-    [&](const std::string &reference_id) -> object_creation_referencet & {
-    auto it = references.find(reference_id);
-    INVARIANT(it != references.end(), "reference id must be present in map");
-    return it->second;
-  };
-  const auto code_with_references = assign_from_json_rec(expr, json, {}, info);
+  code_with_references_listt code_with_references =
+    assign_from_json_rec(expr, json, {}, info);
+  code_blockt assignments;
   allocate.declare_created_symbols(assignments);
-  for(const auto &code_with_ref : code_with_references.list)
-    assignments.append(code_with_ref->to_code(reference_substitution));
+  std::for_each(
+    assignments.statements().rbegin(),
+    assignments.statements().rend(),
+    [&](const codet &c) {
+      code_with_references.add_to_front(code_without_referencest{c});
+    });
+  return code_with_references;
 }

jbmc/src/java_bytecode/assignments_from_json.h

@@ -96,11 +96,10 @@ class ci_lazy_methods_neededt;
 ///   a function, not a line number.
 ///
 /// For parameter documentation, see \ref object_creation_infot.
-void assign_from_json(
+code_with_references_listt assign_from_json(
   const exprt &expr,
   const jsont &json,
   const irep_idt &function_id,
-  code_blockt &block,
   symbol_table_baset &symbol_table,
   optionalt<ci_lazy_methods_neededt> &needed_lazy_methods,
   size_t max_user_array_length,

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -822,19 +822,27 @@ code_blockt get_user_specified_clinit_body(
         }
       }
     }
-    code_blockt body;
+    code_with_references_listt code_with_references;
     for(const auto &value_pair : static_field_values)
     {
-      assign_from_json(
+      code_with_references.append(assign_from_json(
         value_pair.first,
         value_pair.second,
         real_clinit_name,
-        body,
         symbol_table,
         needed_lazy_methods,
         max_user_array_length,
-        references);
+        references));
     }
+    code_with_referencest::reference_substitutiont reference_substitution =
+      [&](const std::string &reference_id) -> object_creation_referencet & {
+      auto it = references.find(reference_id);
+      INVARIANT(it != references.end(), "reference id must be present in map");
+      return it->second;
+    };
+    code_blockt body;
+    for(const auto &code_with_ref : code_with_references.list)
+      body.append(code_with_ref->to_code(reference_substitution));
     return body;
   }
   return code_blockt{{code_function_callt{clinit_func->symbol_expr()}}};

jbmc/unit/java_bytecode/java_static_initializers/assignments_from_json.cpp

@@ -89,17 +89,23 @@ SCENARIO(
 
     const reference_typet test_class_type =
       reference_type(struct_tag_typet{"java::TestClass"});
-    code_blockt block;
     optionalt<ci_lazy_methods_neededt> option{};
-    assign_from_json(
+    const code_with_references_listt code = assign_from_json(
       symbol_exprt{"symbol_to_assign", test_class_type},
       json,
       clinit_name,
-      block,
       symbol_table,
       option,
       max_user_array_length,
       references);
+
+    code_with_referencest::reference_substitutiont reference_substitution =
+      [&](const std::string &reference_id) -> object_creation_referencet & {
+      UNREACHABLE;
+    };
+    code_blockt block;
+    for(auto code_with_references : code.list)
+      block.append(code_with_references->to_code(reference_substitution));
     THEN("The instruction is the declaration of a symbol of TestClass* type")
     {
       const symbol_exprt declared_symbol =
@@ -175,18 +181,24 @@ SCENARIO(
 
     const reference_typet test_class_type =
       reference_type(struct_tag_typet{"java::TestClass"});
-    code_blockt block;
     optionalt<ci_lazy_methods_neededt> option{};
-    assign_from_json(
+    const code_with_references_listt code = assign_from_json(
       symbol_exprt{"symbol_to_assign", test_class_type},
       json,
       clinit_name,
-      block,
       symbol_table,
       option,
       max_user_array_length,
       references);
 
+    code_with_referencest::reference_substitutiont reference_substitution =
+      [&](const std::string &reference_id) -> object_creation_referencet & {
+      UNREACHABLE;
+    };
+    code_blockt block;
+    for(auto code_with_references : code.list)
+      block.append(code_with_references->to_code(reference_substitution));
+
     THEN("The instruction is the declaration of a symbol of TestClass* type")
     {
       const symbol_exprt allocation_symbol =
@@ -294,18 +306,24 @@ SCENARIO(
 
     const reference_typet test_class_type =
       reference_type(struct_tag_typet{"java::TestClass"});
-    code_blockt block;
     optionalt<ci_lazy_methods_neededt> option{};
-    assign_from_json(
+    const code_with_references_listt code = assign_from_json(
       symbol_exprt{"symbol_to_assign", test_class_type},
       json,
       clinit_name,
-      block,
       symbol_table,
       option,
       max_user_array_length,
       references);
 
+    code_with_referencest::reference_substitutiont reference_substitution =
+      [&](const std::string &reference_id) -> object_creation_referencet & {
+      UNREACHABLE;
+    };
+    code_blockt block;
+    for(auto code_with_references : code.list)
+      block.append(code_with_references->to_code(reference_substitution));
+
     THEN("The instruction is the declaration of a symbol of TestClass* type")
     {
       const symbol_exprt allocation_symbol =