Add a class for code with references

This will be use in assign_from_json for json files in which the "@ref"
and "@id" entries are used, so that we can easily substitute code marked
by "@ref" by the code corresponding to the object marked by "@id".

This also move object_creation_referencet to the new header file since
it will be used there, and the allocate_array is now declared in the new
header and defined in the corresponding cpp file.

Author: romainbrenguier

jbmc/src/java_bytecode/code_with_references.cpp

@@ -23,3 +23,43 @@ codet allocate_array(
   java_new_array.type().subtype().set(ID_element_type, element_type);
   return code_assignt{expr, java_new_array, loc};
 }
+
+code_blockt
+reference_allocationt::to_code(reference_substitutiont &references) const
+{
+  const object_creation_referencet &reference = references(reference_id);
+  INVARIANT(reference.array_length, "Length of reference array must be known");
+  if(can_cast_expr<constant_exprt>(*reference.array_length))
+  {
+    return code_blockt(
+      {allocate_array(reference.expr, *reference.array_length, loc)});
+  }
+  // Fallback in case the array definition has not been seen yet, this can
+  // happen if `to_code` is called before the whole json file has been processed
+  // or the "@id" json field corresponding to `reference_id` doesn't appear in
+  // the file.
+  code_blockt code;
+  code.add(code_assignt{*reference.array_length,
+                        side_effect_expr_nondett{java_int_type()}});
+  code.add(code_assumet{binary_predicate_exprt{
+    *reference.array_length, ID_ge, from_integer(0, java_int_type())}});
+  code.add(allocate_array(reference.expr, *reference.array_length, loc));
+  return code;
+}
+
+void code_with_references_listt::add(code_without_referencest code)
+{
+  auto ptr = std::make_shared<code_without_referencest>(std::move(code));
+  list.emplace_back(std::move(ptr));
+}
+
+void code_with_references_listt::add(reference_allocationt ref)
+{
+  auto ptr = std::make_shared<reference_allocationt>(std::move(ref));
+  list.emplace_back(std::move(ptr));
+}
+
+void code_with_references_listt::append(code_with_references_listt &&other)
+{
+  list.splice(list.end(), other.list);
+}

jbmc/src/java_bytecode/code_with_references.h

@@ -33,4 +33,72 @@ struct object_creation_referencet
   optionalt<exprt> array_length;
 };
 
+/// Base class for code which can contain references which can get replaced
+/// before generating actual codet.
+/// Currently only references in array allocations are supported, because this
+/// is currently the only use required by \ref assign_from_json.
+class code_with_referencest
+{
+public:
+  using reference_substitutiont =
+    std::function<const object_creation_referencet &(const std::string &)>;
+
+  virtual code_blockt to_code(reference_substitutiont &) const = 0;
+
+  virtual ~code_with_referencest() = default;
+};
+
+/// Code that should not contain reference
+class code_without_referencest : public code_with_referencest
+{
+public:
+  codet code;
+
+  explicit code_without_referencest(codet code) : code(std::move(code))
+  {
+  }
+
+  code_blockt to_code(reference_substitutiont &) const override
+  {
+    return code_blockt({code});
+  }
+};
+
+/// Allocation code which contains a reference.
+/// The generated code will be of the form:
+///
+///         array_length = nondet(int)
+///         assume(array_length >= 0)
+///         array_expr = new array_type[array_length];
+///
+/// Where array_length and array_expr are given by the reference substitution
+/// function.
+class reference_allocationt : public code_with_referencest
+{
+public:
+  std::string reference_id;
+  source_locationt loc;
+
+  reference_allocationt(std::string reference_id, source_locationt loc)
+    : reference_id(std::move(reference_id)), loc(std::move(loc))
+  {
+  }
+
+  code_blockt to_code(reference_substitutiont &references) const override;
+};
+
+/// Wrapper around a list of shared pointer to code_with_referencest objects,
+/// which provides a nicer interface.
+class code_with_references_listt
+{
+public:
+  std::list<std::shared_ptr<code_with_referencest>> list;
+
+  void add(code_without_referencest code);
+
+  void add(reference_allocationt ref);
+
+  void append(code_with_references_listt &&other);
+};
+
 #endif // CPROVER_JAVA_BYTECODE_CODE_WITH_REFERENCES_H