java_object_factory.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#include "java_object_factory.h"
 
#include <util/arith_tools.h>
#include <util/array_element_from_pointer.h>
#include <util/expr_initializer.h>
#include <util/fresh_symbol.h>
#include <util/message.h>
#include <util/nondet_bool.h>
#include <util/prefix.h>
 
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_functions.h>
#include <util/interval_constraint.h>
 
#include "generic_parameter_specialization_map_keys.h"
#include "java_object_factory_parameters.h"
#include "java_static_initializers.h"
#include "java_string_library_preprocess.h"
#include "java_string_literals.h"
#include "java_utils.h"
#include "select_pointer_type.h"
 
class java_object_factoryt
{
  const java_object_factory_parameterst object_factory_parameters;
 
  std::unordered_set<irep_idt> recursion_set;
 
  generic_parameter_specialization_mapt generic_parameter_specialization_map;
 
  symbol_table_baset &symbol_table;
 
  const select_pointer_typet &pointer_type_selector;
 
  allocate_objectst allocate_objects;
 
  messaget log;
 
  void gen_pointer_target_init(
    code_blockt &assignments,
    const exprt &expr,
    const typet &target_type,
    lifetimet lifetime,
    size_t depth,
    update_in_placet update_in_place,
    const source_locationt &location);
public:
  java_object_factoryt(
    const source_locationt &loc,
    const java_object_factory_parameterst _object_factory_parameters,
    symbol_table_baset &_symbol_table,
    const select_pointer_typet &pointer_type_selector,
    message_handlert &log)
    : object_factory_parameters(_object_factory_parameters),
      symbol_table(_symbol_table),
      pointer_type_selector(pointer_type_selector),
      allocate_objects(
        ID_java,
        loc,
        object_factory_parameters.function_id,
        symbol_table),
      log(log)
  {}
 
  bool gen_nondet_enum_init(
    code_blockt &assignments,
    const exprt &expr,
    const java_class_typet &java_class_type,
    const source_locationt &location);
 
  void gen_nondet_init(
    code_blockt &assignments,
    const exprt &expr,
    bool is_sub,
    bool skip_classid,
    lifetimet lifetime,
    const optionalt<typet> &override_type,
    size_t depth,
    update_in_placet,
    const source_locationt &location);
 
  void add_created_symbol(const symbolt &symbol);
 
  void declare_created_symbols(code_blockt &init_code);
 
private:
  void gen_nondet_pointer_init(
    code_blockt &assignments,
    const exprt &expr,
    lifetimet lifetime,
    const pointer_typet &pointer_type,
    size_t depth,
    const update_in_placet &update_in_place,
    const source_locationt &location);
 
  void gen_nondet_struct_init(
    code_blockt &assignments,
    const exprt &expr,
    bool is_sub,
    bool skip_classid,
    lifetimet lifetime,
    const struct_typet &struct_type,
    size_t depth,
    const update_in_placet &update_in_place,
    const source_locationt &location);
 
  symbol_exprt gen_nondet_subtype_pointer_init(
    code_blockt &assignments,
    lifetimet lifetime,
    const pointer_typet &substitute_pointer_type,
    size_t depth,
    const source_locationt &location);
 
  code_blockt assign_element(
    const exprt &element,
    update_in_placet update_in_place,
    const typet &element_type,
    size_t depth,
    const source_locationt &location);
};
 
void java_object_factoryt::gen_pointer_target_init(
  code_blockt &assignments,
  const exprt &expr,
  const typet &target_type,
  lifetimet lifetime,
  size_t depth,
  update_in_placet update_in_place,
  const source_locationt &location)
{
  PRECONDITION(expr.type().id() == ID_pointer);
  PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
 
  const namespacet ns(symbol_table);
  const typet &followed_target_type = ns.follow(target_type);
  PRECONDITION(followed_target_type.id() == ID_struct);
 
  const auto &target_class_type = to_java_class_type(followed_target_type);
  if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
  {
    assignments.append(gen_nondet_array_init(
      expr,
      update_in_place,
      location,
      [this, update_in_place, depth, location](
        const exprt &element, const typet &element_type) -> code_blockt {
        return assign_element(
          element, update_in_place, element_type, depth + 1, location);
      },
      [this](const typet &type, std::string basename_prefix) -> symbol_exprt {
        return allocate_objects.allocate_automatic_local_object(
          type, basename_prefix);
      },
      symbol_table,
      object_factory_parameters.max_nondet_array_length));
    return;
  }
  if(target_class_type.get_base("java::java.lang.Enum"))
  {
    if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
      return;
  }
 
  // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
  // initialize the fields of the object pointed by `expr`; if in
  // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
  // (return value of `allocate_object`), emit a statement of the form
  // `<expr> := address-of(<new-object>)` and recursively initialize such new
  // object.
  exprt init_expr;
  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
  {
    init_expr = allocate_objects.allocate_object(
      assignments, expr, target_type, lifetime, "tmp_object_factory");
  }
  else
  {
    if(expr.id() == ID_address_of)
      init_expr = to_address_of_expr(expr).object();
    else
    {
      init_expr = dereference_exprt(expr);
    }
  }
 
  gen_nondet_init(
    assignments,
    init_expr,
    false, // is_sub
    false, // skip_classid
    lifetime,
    {}, // no override type
    depth + 1,
    update_in_place,
    location);
}
 
class recursion_set_entryt
{
  std::unordered_set<irep_idt> &recursion_set;
  irep_idt erase_entry;
 
public:
  explicit recursion_set_entryt(std::unordered_set<irep_idt> &_recursion_set)
    : recursion_set(_recursion_set)
  { }
 
  ~recursion_set_entryt()
  {
    if(!erase_entry.empty())
      recursion_set.erase(erase_entry);
  }
 
  recursion_set_entryt(const recursion_set_entryt &)=delete;
  recursion_set_entryt &operator=(const recursion_set_entryt &)=delete;
 
  bool insert_entry(const irep_idt &entry)
  {
    INVARIANT(erase_entry.empty(), "insert_entry should only be called once");
    INVARIANT(!entry.empty(), "entry should be a struct tag");
    bool ret=recursion_set.insert(entry).second;
    if(ret)
    {
      // We added something, so erase it when this is destroyed:
      erase_entry=entry;
    }
    return ret;
  }
};
 
const integer_intervalt printable_char_range(' ', '~');
 
static irep_idt integer_interval_to_string(const integer_intervalt &interval)
{
  std::string result;
  result += numeric_cast_v<char>(interval.lower);
  result += "-";
  result += numeric_cast_v<char>(interval.upper);
  return result;
}
 
void initialize_nondet_string_fields(
  struct_exprt &struct_expr,
  code_blockt &code,
  const std::size_t &min_nondet_string_length,
  const std::size_t &max_nondet_string_length,
  const source_locationt &loc,
  const irep_idt &function_id,
  symbol_table_baset &symbol_table,
  bool printable,
  allocate_objectst &allocate_objects)
{
  namespacet ns(symbol_table);
  const struct_typet &struct_type =
    to_struct_type(ns.follow(struct_expr.type()));
  PRECONDITION(is_java_string_type(struct_type));
 
  // We allow type StringBuffer and StringBuilder to be initialized
  // in the same way has String, because they have the same structure and
  // are treated in the same way by CBMC.
 
  // Note that CharSequence cannot be used as classid because it's abstract,
  // so it is replaced by String.
  // \todo allow StringBuffer and StringBuilder as classid for Charsequence
  if(struct_type.get_tag() == "java.lang.CharSequence")
  {
    set_class_identifier(
      struct_expr, ns, struct_tag_typet("java::java.lang.String"));
  }
 
  // OK, this is a String type with the expected fields -- add code to `code`
  // to set up pre-requisite variables and assign them in `struct_expr`.
 
  // length_expr = nondet(int);
  const symbol_exprt length_expr =
    allocate_objects.allocate_automatic_local_object(
      java_int_type(), "tmp_object_factory");
  const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
  code.add(code_frontend_assignt(length_expr, nondet_length));
 
  // assume (length_expr >= min_nondet_string_length);
  const exprt min_length =
    from_integer(min_nondet_string_length, java_int_type());
  code.add(code_assumet(binary_relation_exprt(length_expr, ID_ge, min_length)));
 
  // assume (length_expr <= max_input_length)
  if(
    max_nondet_string_length <=
    to_integer_bitvector_type(length_expr.type()).largest())
  {
    exprt max_length =
      from_integer(max_nondet_string_length, length_expr.type());
    code.add(
      code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
  }
 
  const exprt data_expr =
    make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
  struct_expr.operands()[struct_type.component_number("length")] = length_expr;
 
  const address_of_exprt array_pointer(
    index_exprt(data_expr, from_integer(0, java_int_type())));
 
  add_pointer_to_array_association(
    array_pointer, data_expr, symbol_table, loc, function_id, code);
 
  add_array_to_length_association(
    data_expr, length_expr, symbol_table, loc, function_id, code);
 
  struct_expr.operands()[struct_type.component_number("data")] = array_pointer;
 
  // Printable ASCII characters are between ' ' and '~'.
  if(printable)
  {
    add_character_set_constraint(
      array_pointer,
      length_expr,
      integer_interval_to_string(printable_char_range),
      symbol_table,
      loc,
      function_id,
      code);
  }
}
 
void java_object_factoryt::gen_nondet_pointer_init(
  code_blockt &assignments,
  const exprt &expr,
  lifetimet lifetime,
  const pointer_typet &pointer_type,
  size_t depth,
  const update_in_placet &update_in_place,
  const source_locationt &location)
{
  PRECONDITION(expr.type().id()==ID_pointer);
  const namespacet ns(symbol_table);
  const typet &subtype = pointer_type.base_type();
  const typet &followed_subtype = ns.follow(subtype);
  PRECONDITION(followed_subtype.id() == ID_struct);
  const pointer_typet &replacement_pointer_type =
    pointer_type_selector.convert_pointer_type(
      pointer_type, generic_parameter_specialization_map, ns);
 
  // If we are changing the pointer, we generate code for creating a pointer
  // to the substituted type instead
  // TODO if we are comparing array types we need to compare their element
  //   types. this is for now done by implementing equality function especially
  //   for java types, technical debt TG-2707
  if(!equal_java_types(replacement_pointer_type, pointer_type))
  {
    // update generic_parameter_specialization_map for the new pointer
    generic_parameter_specialization_map_keyst
      generic_parameter_specialization_map_keys(
        generic_parameter_specialization_map);
    generic_parameter_specialization_map_keys.insert(
      replacement_pointer_type,
      ns.follow(replacement_pointer_type.base_type()));
 
    const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
      assignments, lifetime, replacement_pointer_type, depth, location);
 
    // Having created a pointer to object of type replacement_pointer_type
    // we now assign it back to the original pointer with a cast
    // from pointer_type to replacement_pointer_type
    assignments.add(code_frontend_assignt(
      expr, typecast_exprt(real_pointer_symbol, pointer_type)));
    return;
  }
 
  // This deletes the recursion set entry on leaving this function scope,
  // if one is set below.
  recursion_set_entryt recursion_set_entry(recursion_set);
 
  // We need to prevent the possibility of this code to loop infinitely when
  // initializing a data structure with recursive types or unbounded depth.  We
  // implement two mechanisms here. We keep a set of 'types seen', and
  // detect when we perform a 2nd visit to the same type.  We also detect the
  // depth in the chain of (recursive) calls to the methods of this class.
  // The depth counter is incremented only when a pointer is deferenced,
  // including pointers to arrays.
  //
  // When we visit for 2nd time a type AND the maximum depth is exceeded, we set
  // the pointer to NULL instead of recursively initializing the struct to which
  // it points.
  const struct_typet &struct_type = to_struct_type(followed_subtype);
  const irep_idt &struct_tag = struct_type.get_tag();
 
  // If this is a recursive type of some kind AND the depth is exceeded, set
  // the pointer to null.
  if(
    !recursion_set_entry.insert_entry(struct_tag) &&
    depth >= object_factory_parameters.max_nondet_tree_depth)
  {
    if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
    {
      assignments.add(code_frontend_assignt{
        expr, null_pointer_exprt{pointer_type}, location});
    }
    // Otherwise leave it as it is.
    return;
  }
 
  // If we may be about to initialize a non-null enum type, always run the
  // clinit_wrapper of its class first.
  // TODO: TG-4689 we may want to do this for all types, not just enums, as
  // described in the Java language specification:
  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
  // But we would have to put this behavior behind an option as it would have an
  // impact on running times.
  // Note that it would be more consistent with the behaviour of the JVM to only
  // run clinit_wrapper if we are about to initialize an object of which we know
  // for sure that it is not null on any following branch. However, adding this
  // case in gen_nondet_struct_init would slow symex down too much, so if we
  // decide to do this for all types, we should do it here.
  // Note also that this logic is mirrored in
  // ci_lazy_methodst::initialize_instantiated_classes.
  if(
    const auto class_type =
      type_try_dynamic_cast<java_class_typet>(followed_subtype))
  {
    if(class_type->get_base("java::java.lang.Enum"))
    {
      const irep_idt &class_name = class_type->get_name();
      const irep_idt class_clinit = clinit_wrapper_name(class_name);
      if(const auto clinit_func = symbol_table.lookup(class_clinit))
        assignments.add(code_function_callt{clinit_func->symbol_expr()});
    }
  }
 
  code_blockt new_object_assignments;
  code_blockt update_in_place_assignments;
 
  // if the initialization mode is MAY_UPDATE or MUST_UPDATE in place, then we
  // emit to `update_in_place_assignments` code for in-place initialization of
  // the object pointed by `expr`, assuming that such object is of type
  // `subtype`
  if(update_in_place!=update_in_placet::NO_UPDATE_IN_PLACE)
  {
    gen_pointer_target_init(
      update_in_place_assignments,
      expr,
      subtype,
      lifetime,
      depth,
      update_in_placet::MUST_UPDATE_IN_PLACE,
      location);
  }
 
  // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
  // above to `assignments` and return
  if(update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE)
  {
    assignments.append(update_in_place_assignments);
    return;
  }
 
  // if the mode is NO_UPDATE or MAY_UPDATE in place, then we need to emit a
  // vector of assignments that create a new object (recursively initializes it)
  // and asign to `expr` the address of such object
  code_blockt non_null_inst;
 
  gen_pointer_target_init(
    non_null_inst,
    expr,
    subtype,
    lifetime,
    depth,
    update_in_placet::NO_UPDATE_IN_PLACE,
    location);
 
  const code_frontend_assignt set_null_inst{
    expr, null_pointer_exprt{pointer_type}, location};
 
  const bool allow_null = depth > object_factory_parameters.min_null_tree_depth;
 
  if(!allow_null)
  {
    // Add the following code to assignments:
    // <expr> = <aoe>;
    new_object_assignments.append(non_null_inst);
  }
  else
  {
    // if(NONDET(_Bool)
    // {
    //    <expr> = <null pointer>
    // }
    // else
    // {
    //    <code from recursive call to gen_nondet_init() with
    //             tmp$<temporary_counter>>
    // }
    code_ifthenelset null_check(
      side_effect_expr_nondett(bool_typet(), location),
      std::move(set_null_inst),
      std::move(non_null_inst));
 
    new_object_assignments.add(std::move(null_check));
  }
 
  // Similarly to above, maybe use a conditional if both the
  // allocate-fresh and update-in-place cases are allowed:
  if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
  {
    assignments.append(new_object_assignments);
  }
  else
  {
    INVARIANT(update_in_place==update_in_placet::MAY_UPDATE_IN_PLACE,
      "No-update and must-update should have already been resolved");
 
    code_ifthenelset update_check(
      side_effect_expr_nondett(bool_typet(), expr.source_location()),
      std::move(update_in_place_assignments),
      std::move(new_object_assignments));
 
    assignments.add(std::move(update_check));
  }
}
 
symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
  code_blockt &assignments,
  lifetimet lifetime,
  const pointer_typet &replacement_pointer,
  size_t depth,
  const source_locationt &location)
{
  const symbol_exprt new_symbol_expr =
    allocate_objects.allocate_automatic_local_object(
      replacement_pointer, "tmp_object_factory");
 
  // Generate a new object into this new symbol
  gen_nondet_init(
    assignments,
    new_symbol_expr,
    false, // is_sub
    false, // skip_classid
    lifetime,
    {}, // no override_type
    depth,
    update_in_placet::NO_UPDATE_IN_PLACE,
    location);
 
  return new_symbol_expr;
}
 
alternate_casest get_string_input_values_code(
  const exprt &expr,
  const std::list<std::string> &string_input_values,
  symbol_table_baset &symbol_table)
{
  alternate_casest cases;
  for(const auto &val : string_input_values)
  {
    const symbol_exprt s =
      get_or_create_string_literal_symbol(val, symbol_table, true);
    cases.push_back(code_frontend_assignt(expr, s));
  }
  return cases;
}
 
void java_object_factoryt::gen_nondet_struct_init(
  code_blockt &assignments,
  const exprt &expr,
  bool is_sub,
  bool skip_classid,
  lifetimet lifetime,
  const struct_typet &struct_type,
  size_t depth,
  const update_in_placet &update_in_place,
  const source_locationt &location)
{
  const namespacet ns(symbol_table);
  PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
 
  typedef struct_typet::componentst componentst;
  const irep_idt &struct_tag=struct_type.get_tag();
 
  const componentst &components=struct_type.components();
 
  // Should we write the whole object?
  // * Not if this is a sub-structure (a superclass object), as our caller will
  //   have done this already
  // * Not if the object has already been initialised by our caller, in which
  //   case they will set `skip_classid`
  // * Not if we're re-initializing an existing object (i.e. update_in_place)
  // * Always if it has a string type. Strings should not be partially updated,
  //   and the `length` and `data` components of string types need to be
  //   generated differently from object fields in the general case, see
  //   \ref java_object_factoryt::initialize_nondet_string_fields.
 
  const bool has_string_input_values =
    !object_factory_parameters.string_input_values.empty();
 
  if(
    is_java_string_type(struct_type) && has_string_input_values &&
    !skip_classid)
  { // We're dealing with a string and we should set fixed input values.
    // We create a switch statement where each case is an assignment
    // of one of the fixed input strings to the input variable in question
    const alternate_casest cases = get_string_input_values_code(
      expr, object_factory_parameters.string_input_values, symbol_table);
    assignments.add(generate_nondet_switch(
      id2string(object_factory_parameters.function_id),
      cases,
      java_int_type(),
      ID_java,
      location,
      symbol_table));
  }
  else if(
    (!is_sub && !skip_classid &&
     update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) ||
    is_java_string_type(struct_type))
  {
    // Add an initial all-zero write. Most of the fields of this will be
    // overwritten, but it helps to have a whole-structure write that analysis
    // passes can easily recognise leaves no uninitialised state behind.
 
    // This code mirrors the `remove_java_new` pass:
    auto initial_object = zero_initializer(expr.type(), source_locationt(), ns);
    CHECK_RETURN(initial_object.has_value());
    set_class_identifier(
      to_struct_expr(*initial_object),
      ns,
      struct_tag_typet("java::" + id2string(struct_tag)));
 
    // If the initialised type is a special-cased String type (one with length
    // and data fields introduced by string-library preprocessing), initialise
    // those fields with nondet values
    if(is_java_string_type(struct_type))
    { // We're dealing with a string
      initialize_nondet_string_fields(
        to_struct_expr(*initial_object),
        assignments,
        object_factory_parameters.min_nondet_string_length,
        object_factory_parameters.max_nondet_string_length,
        location,
        object_factory_parameters.function_id,
        symbol_table,
        object_factory_parameters.string_printable,
        allocate_objects);
    }
 
    assignments.add(code_frontend_assignt(expr, *initial_object));
  }
 
  for(const auto &component : components)
  {
    const typet &component_type=component.type();
    irep_idt name=component.get_name();
 
    member_exprt me(expr, name, component_type);
 
    if(name == JAVA_CLASS_IDENTIFIER_FIELD_NAME)
    {
      continue;
    }
    else if(name == "cproverMonitorCount")
    {
      // Zero-initialize 'cproverMonitorCount' field as it is not meant to be
      // nondet. This field is only present when the java core models are
      // included in the class-path. It is used to implement a critical section,
      // which is necessary to support concurrency.
      if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE)
        continue;
      code_frontend_assignt code(me, from_integer(0, me.type()));
      code.add_source_location() = location;
      assignments.add(code);
    }
    else if(
      is_java_string_type(struct_type) && (name == "length" || name == "data"))
    {
      // In this case these were set up above.
      continue;
    }
    else
    {
      INVARIANT(!name.empty(), "Each component of a struct must have a name");
 
      bool _is_sub=name[0]=='@';
 
      // MUST_UPDATE_IN_PLACE only applies to this object.
      // If this is a pointer to another object, offer the chance
      // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
      update_in_placet substruct_in_place=
        update_in_place==update_in_placet::MUST_UPDATE_IN_PLACE && !_is_sub ?
        update_in_placet::MAY_UPDATE_IN_PLACE :
        update_in_place;
      gen_nondet_init(
        assignments,
        me,
        _is_sub,
        false, // skip_classid
        lifetime,
        {}, // no override_type
        depth,
        substruct_in_place,
        location);
    }
  }
 
  // If cproverNondetInitialize() can be found in the symbol table as a method
  // on this class or any parent, we add a call:
  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  // expr.cproverNondetInitialize();
  // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
  resolve_inherited_componentt resolve_inherited_component{symbol_table};
  optionalt<resolve_inherited_componentt::inherited_componentt>
    cprover_nondet_initialize = resolve_inherited_component(
      "java::" + id2string(struct_tag), "cproverNondetInitialize:()V", true);
 
  if(cprover_nondet_initialize)
  {
    const symbolt &cprover_nondet_initialize_symbol =
      ns.lookup(cprover_nondet_initialize->get_full_component_identifier());
    assignments.add(
      code_function_callt{cprover_nondet_initialize_symbol.symbol_expr(),
                          {address_of_exprt{expr}}});
  }
}
 
static code_blockt assume_expr_integral(
  const exprt &expr,
  const typet &type,
  const source_locationt &location,
  const allocate_local_symbolt &allocate_local_symbol)
{
  PRECONDITION(type == java_float_type() || type == java_double_type());
 
  code_blockt assignments;
 
  const auto &aux_int =
    allocate_local_symbol(java_int_type(), "assume_integral_tmp");
  assignments.add(code_declt(aux_int), location);
  exprt nondet_rhs = side_effect_expr_nondett(java_int_type(), location);
  code_frontend_assignt aux_assign(aux_int, nondet_rhs);
  aux_assign.add_source_location() = location;
  assignments.add(aux_assign);
  assignments.add(
    code_assumet(equal_exprt(typecast_exprt(aux_int, type), expr)));
 
  return assignments;
}
 
void java_object_factoryt::gen_nondet_init(
  code_blockt &assignments,
  const exprt &expr,
  bool is_sub,
  bool skip_classid,
  lifetimet lifetime,
  const optionalt<typet> &override_type,
  size_t depth,
  update_in_placet update_in_place,
  const source_locationt &location)
{
  const typet &type = override_type.has_value() ? *override_type : expr.type();
  const namespacet ns(symbol_table);
  const typet &followed_type = ns.follow(type);
 
  if(type.id()==ID_pointer)
  {
    // dereferenced type
    const pointer_typet &pointer_type=to_pointer_type(type);
 
    // If we are about to initialize a generic pointer type, add its concrete
    // types to the map and delete them on leaving this function scope.
    generic_parameter_specialization_map_keyst
      generic_parameter_specialization_map_keys(
        generic_parameter_specialization_map);
    generic_parameter_specialization_map_keys.insert(
      pointer_type, ns.follow(pointer_type.base_type()));
 
    gen_nondet_pointer_init(
      assignments,
      expr,
      lifetime,
      pointer_type,
      depth,
      update_in_place,
      location);
  }
  else if(followed_type.id() == ID_struct)
  {
    const struct_typet struct_type = to_struct_type(followed_type);
 
    // If we are about to initialize a generic class (as a superclass object
    // for a different object), add its concrete types to the map and delete
    // them on leaving this function scope.
    generic_parameter_specialization_map_keyst
      generic_parameter_specialization_map_keys(
        generic_parameter_specialization_map);
    if(is_sub)
    {
      const typet &symbol =
        override_type.has_value() ? *override_type : expr.type();
      PRECONDITION(symbol.id() == ID_struct_tag);
      generic_parameter_specialization_map_keys.insert(
        to_struct_tag_type(symbol), struct_type);
    }
 
    gen_nondet_struct_init(
      assignments,
      expr,
      is_sub,
      skip_classid,
      lifetime,
      struct_type,
      depth,
      update_in_place,
      location);
  }
  else
  {
    // types different from pointer or structure:
    // bool, int, float, byte, char, ...
    exprt rhs = type.id() == ID_c_bool
                  ? get_nondet_bool(type, location)
                  : side_effect_expr_nondett(type, location);
    code_frontend_assignt assign(expr, rhs);
    assign.add_source_location() = location;
 
    assignments.add(assign);
    if(type == java_char_type() && object_factory_parameters.string_printable)
    {
      assignments.add(
        code_assumet(interval_constraint(expr, printable_char_range)));
    }
    // add assumes to obey numerical restrictions
    if(type != java_boolean_type() && type != java_char_type())
    {
      const auto &interval = object_factory_parameters.assume_inputs_interval;
      if(auto singleton = interval.as_singleton())
      {
        assignments.add(
          code_frontend_assignt{expr, from_integer(*singleton, expr.type())});
      }
      else
      {
        exprt within_bounds = interval.make_contains_expr(expr);
        if(!within_bounds.is_true())
          assignments.add(code_assumet(std::move(within_bounds)));
      }
 
      if(
        object_factory_parameters.assume_inputs_integral &&
        (type == java_float_type() || type == java_double_type()))
      {
        assignments.add(assume_expr_integral(
          expr,
          type,
          location,
          [this](
            const typet &type, std::string basename_prefix) -> symbol_exprt {
            return allocate_objects.allocate_automatic_local_object(
              type, basename_prefix);
          }));
      }
    }
  }
}
 
void java_object_factoryt::add_created_symbol(const symbolt &symbol)
{
  allocate_objects.add_created_symbol(symbol);
}
 
void java_object_factoryt::declare_created_symbols(code_blockt &init_code)
{
  allocate_objects.declare_created_symbols(init_code);
}
 
static void allocate_nondet_length_array(
  code_blockt &assignments,
  const exprt &lhs,
  const exprt &max_length_expr,
  const typet &element_type,
  const allocate_local_symbolt &allocate_local_symbol,
  const source_locationt &location)
{
  const auto &length_sym_expr = generate_nondet_int(
    from_integer(0, java_int_type()),
    max_length_expr,
    "nondet_array_length",
    location,
    allocate_local_symbol,
    assignments);
 
  side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), location);
  java_new_array.copy_to_operands(length_sym_expr);
  java_new_array.set(ID_length_upper_bound, max_length_expr);
  to_type_with_subtype(java_new_array.type())
    .subtype()
    .set(ID_element_type, element_type);
  code_frontend_assignt assign(lhs, java_new_array);
  assign.add_source_location() = location;
  assignments.add(assign);
}
 
static void array_primitive_init_code(
  code_blockt &assignments,
  const exprt &init_array_expr,
  const typet &element_type,
  const exprt &max_length_expr,
  const source_locationt &location,
  const allocate_local_symbolt &allocate_local_symbol)
{
  const array_typet array_type(element_type, max_length_expr);
 
  // TYPE (*array_data_init)[max_length_expr];
  const symbol_exprt &tmp_finite_array_pointer =
    allocate_local_symbol(pointer_type(array_type), "array_data_init");
 
  // array_data_init = ALLOCATE(TYPE [max_length_expr], max_length_expr, false);
  assignments.add(
    make_allocate_code(
      tmp_finite_array_pointer,
      max_length_expr));
  assignments.statements().back().add_source_location() = location;
 
  // *array_data_init = NONDET(TYPE [max_length_expr]);
  side_effect_expr_nondett nondet_data(array_type, location);
  const dereference_exprt data_pointer_deref{tmp_finite_array_pointer};
  assignments.add(
    code_frontend_assignt(data_pointer_deref, std::move(nondet_data)));
  assignments.statements().back().add_source_location() = location;
 
  // init_array_expr = *array_data_init;
  address_of_exprt tmp_nondet_pointer(
    index_exprt(data_pointer_deref, from_integer(0, java_int_type())));
  assignments.add(
    code_frontend_assignt(init_array_expr, std::move(tmp_nondet_pointer)));
  assignments.statements().back().add_source_location() = location;
}
 
code_blockt java_object_factoryt::assign_element(
  const exprt &element,
  const update_in_placet update_in_place,
  const typet &element_type,
  const size_t depth,
  const source_locationt &location)
{
  code_blockt assignments;
  bool new_item_is_primitive = element.type().id() != ID_pointer;
 
  // Use a temporary to initialise a new, or update an existing, non-primitive.
  // This makes it clearer that in a sequence like
  // `new_array_item->x = y; new_array_item->z = w;` that all the
  // `new_array_item` references must alias, cf. the harder-to-analyse
  // `some_expr[idx]->x = y; some_expr[idx]->z = w;`
  exprt init_expr;
  if(new_item_is_primitive)
  {
    init_expr = element;
  }
  else
  {
    init_expr = allocate_objects.allocate_automatic_local_object(
      element.type(), "new_array_item");
 
    // If we're updating an existing array item, read the existing object that
    // we (may) alter:
    if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
      assignments.add(code_frontend_assignt(init_expr, element));
  }
 
  // MUST_UPDATE_IN_PLACE only applies to this object.
  // If this is a pointer to another object, offer the chance
  // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
  update_in_placet child_update_in_place =
    update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE
      ? update_in_placet::MAY_UPDATE_IN_PLACE
      : update_in_place;
  gen_nondet_init(
    assignments,
    init_expr,
    false, // is_sub
    false, // skip_classid
    // These are variable in number, so use dynamic allocator:
    lifetimet::DYNAMIC,
    element_type, // override
    depth,
    child_update_in_place,
    location);
 
  if(!new_item_is_primitive)
  {
    // We used a temporary variable to update or initialise an array item;
    // now write it into the array:
    assignments.add(code_frontend_assignt(element, init_expr));
  }
  return assignments;
}
 
static void array_loop_init_code(
  code_blockt &assignments,
  const exprt &init_array_expr,
  const exprt &length_expr,
  const typet &element_type,
  const exprt &max_length_expr,
  update_in_placet update_in_place,
  const source_locationt &location,
  const array_element_generatort &element_generator,
  const allocate_local_symbolt &allocate_local_symbol,
  const symbol_tablet &symbol_table)
{
  const symbol_exprt &array_init_symexpr =
    allocate_local_symbol(init_array_expr.type(), "array_data_init");
 
  code_frontend_assignt data_assign(array_init_symexpr, init_array_expr);
  data_assign.add_source_location() = location;
  assignments.add(data_assign);
 
  const symbol_exprt &counter_expr =
    allocate_local_symbol(length_expr.type(), "array_init_iter");
 
  code_blockt loop_body;
  if(update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE)
  {
    // Add a redundant if(counter == max_length) break
    // that is easier for the unwinder to understand.
    code_ifthenelset max_test(
      equal_exprt(counter_expr, max_length_expr), code_breakt{});
 
    loop_body.add(std::move(max_test));
  }
 
  const dereference_exprt element_at_counter =
    array_element_from_pointer(array_init_symexpr, counter_expr);
 
  loop_body.append(element_generator(element_at_counter, element_type));
 
  assignments.add(code_fort::from_index_bounds(
    from_integer(0, java_int_type()),
    length_expr,
    counter_expr,
    std::move(loop_body),
    location));
}
 
code_blockt gen_nondet_array_init(
  const exprt &expr,
  update_in_placet update_in_place,
  const source_locationt &location,
  const array_element_generatort &element_generator,
  const allocate_local_symbolt &allocate_local_symbol,
  const symbol_tablet &symbol_table,
  const size_t max_nondet_array_length)
{
  PRECONDITION(expr.type().id() == ID_pointer);
  PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_struct_tag);
  PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
 
  code_blockt statements;
 
  const namespacet ns(symbol_table);
  const typet &type = ns.follow(to_pointer_type(expr.type()).base_type());
  const struct_typet &struct_type = to_struct_type(type);
  const typet &element_type = static_cast<const typet &>(
    to_pointer_type(expr.type()).base_type().find(ID_element_type));
 
  auto max_length_expr = from_integer(max_nondet_array_length, java_int_type());
 
  // In NO_UPDATE_IN_PLACE mode we allocate a new array and recursively
  // initialize its elements
  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
  {
    allocate_nondet_length_array(
      statements,
      expr,
      max_length_expr,
      element_type,
      allocate_local_symbol,
      location);
  }
 
  // Otherwise we're updating the array in place, and use the
  // existing array allocation and length.
 
  INVARIANT(
    is_valid_java_array(struct_type),
    "Java struct array does not conform to expectations");
 
  dereference_exprt deref_expr(expr);
  const auto &comps = struct_type.components();
  const member_exprt length_expr(deref_expr, "length", comps[1].type());
  exprt init_array_expr = member_exprt(deref_expr, "data", comps[2].type());
 
  if(init_array_expr.type() != pointer_type(element_type))
    init_array_expr =
      typecast_exprt(init_array_expr, pointer_type(element_type));
 
  if(element_type.id() == ID_pointer || element_type.id() == ID_c_bool)
  {
    // For arrays of non-primitive type, nondeterministically initialize each
    // element of the array
    array_loop_init_code(
      statements,
      init_array_expr,
      length_expr,
      element_type,
      max_length_expr,
      update_in_place,
      location,
      element_generator,
      allocate_local_symbol,
      symbol_table);
  }
  else
  {
    // Arrays of primitive type can be initialized with a single instruction.
    // We don't do this for arrays of primitive booleans, because booleans are
    // represented as unsigned bytes, so each cell must be initialized as
    // 0 or 1 (see gen_nondet_init).
    array_primitive_init_code(
      statements,
      init_array_expr,
      element_type,
      max_length_expr,
      location,
      allocate_local_symbol);
  }
  return statements;
}
 
bool java_object_factoryt::gen_nondet_enum_init(
  code_blockt &assignments,
  const exprt &expr,
  const java_class_typet &java_class_type,
  const source_locationt &location)
{
  const irep_idt &class_name = java_class_type.get_name();
  const irep_idt values_name = id2string(class_name) + ".$VALUES";
  if(!symbol_table.has_symbol(values_name))
  {
    log.warning() << values_name
                  << " is missing, so the corresponding Enum "
                     "type will nondet initialised"
                  << messaget::eom;
    return false;
  }
 
  const namespacet ns(symbol_table);
  const symbolt &values = ns.lookup(values_name);
 
  // Access members (length and data) of $VALUES array
  dereference_exprt deref_expr(values.symbol_expr());
  const auto &deref_struct_type = to_struct_type(ns.follow(deref_expr.type()));
  PRECONDITION(is_valid_java_array(deref_struct_type));
  const auto &comps = deref_struct_type.components();
  const member_exprt length_expr(deref_expr, "length", comps[1].type());
  const member_exprt enum_array_expr =
    member_exprt(deref_expr, "data", comps[2].type());
 
  const symbol_exprt &index_expr = generate_nondet_int(
    from_integer(0, java_int_type()),
    minus_exprt(length_expr, from_integer(1, java_int_type())),
    "enum_index_init",
    location,
    allocate_objects,
    assignments);
 
  const dereference_exprt element_at_index =
    array_element_from_pointer(enum_array_expr, index_expr);
  code_frontend_assignt enum_assign(
    expr, typecast_exprt(element_at_index, expr.type()));
  assignments.add(enum_assign);
 
  return true;
}
 
static void assert_type_consistency(const code_blockt &assignments)
{
  // In future we'll be able to use codet::validate for this;
  // at present that only verifies `lhs.type base_type_eq right.type`,
  // whereas we want to check exact equality.
  for(const auto &code : assignments.statements())
  {
    if(code.get_statement() != ID_assign)
      continue;
    const auto &assignment = to_code_frontend_assign(code);
    INVARIANT(
      assignment.lhs().type() == assignment.rhs().type(),
      "object factory should produce type-consistent assignments");
  }
}
 
exprt object_factory(
  const typet &type,
  const irep_idt base_name,
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  java_object_factory_parameterst parameters,
  lifetimet lifetime,
  const source_locationt &loc,
  const select_pointer_typet &pointer_type_selector,
  message_handlert &log)
{
  const symbolt &main_symbol = get_fresh_aux_symbol(
    type,
    id2string(goto_functionst::entry_point()),
    id2string(base_name),
    loc,
    ID_java,
    symbol_table);
 
  parameters.function_id = goto_functionst::entry_point();
 
  exprt object=main_symbol.symbol_expr();
 
  java_object_factoryt state(
    loc, parameters, symbol_table, pointer_type_selector, log);
  code_blockt assignments;
  state.gen_nondet_init(
    assignments,
    object,
    false, // is_sub
    false, // skip_classid
    lifetime,
    {}, // no override_type
    1,  // initial depth
    update_in_placet::NO_UPDATE_IN_PLACE,
    loc);
 
  state.add_created_symbol(main_symbol);
  state.declare_created_symbols(init_code);
 
  assert_type_consistency(assignments);
  init_code.append(assignments);
  return object;
}
 
void gen_nondet_init(
  const exprt &expr,
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  const source_locationt &loc,
  bool skip_classid,
  lifetimet lifetime,
  const java_object_factory_parameterst &object_factory_parameters,
  const select_pointer_typet &pointer_type_selector,
  update_in_placet update_in_place,
  message_handlert &log)
{
  java_object_factoryt state(
    loc, object_factory_parameters, symbol_table, pointer_type_selector, log);
  code_blockt assignments;
  state.gen_nondet_init(
    assignments,
    expr,
    false, // is_sub
    skip_classid,
    lifetime,
    {}, // no override_type
    1,  // initial depth
    update_in_place,
    loc);
 
  state.declare_created_symbols(init_code);
 
  assert_type_consistency(assignments);
  init_code.append(assignments);
}
 
exprt object_factory(
  const typet &type,
  const irep_idt base_name,
  code_blockt &init_code,
  symbol_tablet &symbol_table,
  const java_object_factory_parameterst &object_factory_parameters,
  lifetimet lifetime,
  const source_locationt &location,
  message_handlert &log)
{
  select_pointer_typet pointer_type_selector;
  return object_factory(
    type,
    base_name,
    init_code,
    symbol_table,
    object_factory_parameters,
    lifetime,
    location,
    pointer_type_selector,
    log);
}
 
void gen_nondet_init(
  const exprt &expr,
  code_blockt &init_code,
  symbol_table_baset &symbol_table,
  const source_locationt &loc,
  bool skip_classid,
  lifetimet lifetime,
  const java_object_factory_parameterst &object_factory_parameters,
  update_in_placet update_in_place,
  message_handlert &log)
{
  select_pointer_typet pointer_type_selector;
  gen_nondet_init(
    expr,
    init_code,
    symbol_table,
    loc,
    skip_classid,
    lifetime,
    object_factory_parameters,
    pointer_type_selector,
    update_in_place,
    log);
}