assignments_from_json.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Assignments to values specified in JSON files
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#include "assignments_from_json.h"
 
#include <util/arith_tools.h>
#include <util/array_element_from_pointer.h>
#include <util/expr_initializer.h>
#include <util/ieee_float.h>
#include <util/json.h>
#include <util/symbol_table_base.h>
#include <util/unicode.h>
 
#include <goto-programs/allocate_objects.h>
#include <goto-programs/class_identifier.h>
#include <goto-programs/goto_instruction_code.h>
 
#include "ci_lazy_methods_needed.h"
#include "code_with_references.h"
#include "java_static_initializers.h"
#include "java_string_literals.h"
#include "java_types.h"
#include "java_utils.h"
 
struct object_creation_infot
{
  allocate_objectst &allocate_objects;
 
  symbol_table_baset &symbol_table;
 
  std::optional<ci_lazy_methods_neededt> &needed_lazy_methods;
 
  std::unordered_map<std::string, object_creation_referencet> &references;
 
  const source_locationt &loc;
 
  size_t max_user_array_length;
 
  const java_class_typet &declaring_class_type;
};
 
static java_class_typet
followed_class_type(const exprt &expr, const symbol_table_baset &symbol_table)
{
  const pointer_typet &pointer_type = to_pointer_type(expr.type());
  const java_class_typet &java_class_type = to_java_class_type(
    namespacet{symbol_table}.follow(pointer_type.base_type()));
  return java_class_type;
}
 
static bool
has_enum_type(const exprt &expr, const symbol_table_baset &symbol_table)
{
  return followed_class_type(expr, symbol_table).get_is_enumeration();
}
 
static bool is_enum_with_type_equal_to_declaring_type(
  const exprt &expr,
  const symbol_table_baset &symbol_table,
  const java_class_typet &declaring_class_type)
{
  PRECONDITION(can_cast_type<pointer_typet>(expr.type()));
  return followed_class_type(expr, symbol_table) == declaring_class_type &&
         declaring_class_type.get_is_enumeration();
}
 
static std::optional<std::string> get_type(const jsont &json)
{
  if(!json.is_object())
    return {};
  const auto &json_object = to_json_object(json);
  if(json_object.find("@type") == json_object.end())
    return {};
  return json_object["@type"].value;
}
 
static bool has_id(const jsont &json)
{
  if(!json.is_object())
    return false;
  const auto &json_object = to_json_object(json);
  return json_object.find("@id") != json_object.end();
}
 
static bool is_reference(const jsont &json)
{
  if(!json.is_object())
    return false;
  const auto &json_object = to_json_object(json);
  return json_object.find("@ref") != json_object.end();
}
 
static std::string get_id_or_reference_value(const jsont &json)
{
  PRECONDITION(has_id(json) || is_reference(json));
  if(has_id(json))
    return json["@id"].value;
  return json["@ref"].value;
}
 
static std::string get_enum_id(
  const exprt &expr,
  const jsont &json,
  const symbol_table_baset &symbol_table)
{
  PRECONDITION(json.is_object());
  const auto &json_object = to_json_object(json);
  INVARIANT(
    json_object.find("name") != json_object.end(),
    "JSON representation of enums should include name field");
  return id2string(followed_class_type(expr, symbol_table).get_tag()) + '.' +
         (json["name"].value);
}
 
static bool has_nondet_length(const jsont &json)
{
  if(!json.is_object())
    return false;
  const auto &json_object = to_json_object(json);
  auto nondet_it = json_object.find("@nondetLength");
  return nondet_it != json_object.end() && nondet_it->second.is_true();
}
 
static jsont get_untyped(const jsont &json, const std::string &object_key)
{
  if(!json.is_object())
    return json;
 
  const auto &json_object = to_json_object(json);
  PRECONDITION(
    get_type(json) || json_object.find("@nondetLength") != json_object.end());
 
  return json[object_key];
}
 
static jsont get_untyped_primitive(const jsont &json)
{
  return get_untyped(json, "value");
}
 
static json_arrayt
get_untyped_array(const jsont &json, const typet &element_type)
{
  const jsont untyped = get_untyped(json, "@items");
  PRECONDITION(untyped.is_array());
  const auto &json_array = to_json_array(untyped);
  if(element_type == java_char_type())
  {
    PRECONDITION(json_array.size() == 1);
    const auto &first = *json_array.begin();
    PRECONDITION(first.is_string());
    const auto &json_string = to_json_string(first);
 
    const auto wide_string = utf8_to_utf16_native_endian(json_string.value);
    auto string_range = make_range(wide_string.begin(), wide_string.end());
    const auto json_range = string_range.map([](const wchar_t &c) {
      const std::u16string u16(1, c);
      return json_stringt{utf16_native_endian_to_utf8(u16)};
    });
    return json_arrayt{json_range.begin(), json_range.end()};
  }
  return json_array;
}
 
static jsont get_untyped_string(const jsont &json)
{
  return get_untyped(json, "value");
}
 
static std::optional<java_class_typet> runtime_type(
  const jsont &json,
  const std::optional<std::string> &type_from_array,
  const symbol_table_baset &symbol_table)
{
  const auto type_from_json = get_type(json);
  if(!type_from_json && !type_from_array)
    return {}; // no runtime type specified, use compile-time type
  const auto runtime_type = [&]() -> std::string {
    if(type_from_json)
      return "java::" + *type_from_json;
    INVARIANT(
      type_from_array->find('L') == 0 &&
        type_from_array->rfind(';') == type_from_array->length() - 1,
      "Types inferred from the type of a containing array should be of the "
      "form Lmy.package.name.ClassName;");
    return "java::" + type_from_array->substr(1, type_from_array->length() - 2);
  }();
  if(!symbol_table.has_symbol(runtime_type))
    return {}; // Fall back to compile-time type if runtime type was not found
  const auto &replacement_class_type =
    to_java_class_type(symbol_table.lookup_ref(runtime_type).type);
  return replacement_class_type;
}
 
static std::optional<std::string> element_type_from_array_type(
  const jsont &json,
  const std::optional<std::string> &type_from_array)
{
  if(const auto json_array_type = get_type(json))
  {
    INVARIANT(
      json_array_type->find('[') == 0,
      "Array types in the JSON input should be of the form "
      "[[...[Lmy.package.name.ClassName; (with n occurrences of [ for an "
      "n-dimensional array)");
    return json_array_type->substr(1);
  }
  else if(type_from_array)
  {
    INVARIANT(
      type_from_array->find('[') == 0,
      "For arrays that are themselves contained by an array from which a type "
      "is inferred, such a type should be of the form "
      "[[...[Lmy.package.name.ClassName;");
    return type_from_array->substr(1);
  }
  return {};
}
 
code_with_references_listt assign_from_json_rec(
  const exprt &expr,
  const jsont &json,
  const std::optional<std::string> &type_from_array,
  object_creation_infot &info);
 
static code_with_references_listt
assign_primitive_from_json(const exprt &expr, const jsont &json)
{
  code_with_references_listt result;
  if(json.is_null()) // field is not mentioned in json, leave as default value
    return result;
  if(expr.type() == java_boolean_type())
  {
    result.add(code_frontend_assignt{
      expr, json.is_true() ? (exprt)true_exprt{} : (exprt)false_exprt{}});
  }
  else if(
    expr.type() == java_int_type() || expr.type() == java_byte_type() ||
    expr.type() == java_short_type() || expr.type() == java_long_type())
  {
    result.add(code_frontend_assignt{
      expr, from_integer(std::stoll(json.value), expr.type())});
  }
  else if(expr.type() == java_double_type())
  {
    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
    ieee_float.from_double(std::stod(json.value));
    result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
  }
  else if(expr.type() == java_float_type())
  {
    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
    ieee_float.from_float(std::stof(json.value));
    result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
  }
  else if(expr.type() == java_char_type())
  {
    const std::wstring wide_value = utf8_to_utf16_native_endian(json.value);
    PRECONDITION(wide_value.length() == 1);
    result.add(code_frontend_assignt{
      expr, from_integer(wide_value.front(), expr.type())});
  }
  return result;
}
 
static code_frontend_assignt assign_null(const exprt &expr)
{
  return code_frontend_assignt{
    expr, null_pointer_exprt{to_pointer_type(expr.type())}};
}
 
static code_with_references_listt assign_array_data_component_from_json(
  const exprt &expr,
  const jsont &json,
  const std::optional<std::string> &type_from_array,
  object_creation_infot &info)
{
  const auto &java_class_type = followed_class_type(expr, info.symbol_table);
  const auto &data_component = java_class_type.components()[2];
  const auto &element_type = java_array_element_type(
    to_struct_tag_type(to_pointer_type(expr.type()).base_type()));
  const exprt data_member_expr = typecast_exprt::conditional_cast(
    member_exprt{dereference_exprt{expr}, "data", data_component.type()},
    pointer_type(element_type));
 
  const symbol_exprt &array_init_data =
    info.allocate_objects.allocate_automatic_local_object(
      data_member_expr.type(), "user_specified_array_data_init");
  code_with_references_listt result;
  result.add(
    code_frontend_assignt{array_init_data, data_member_expr, info.loc});
 
  size_t index = 0;
  const std::optional<std::string> inferred_element_type =
    element_type_from_array_type(json, type_from_array);
  const json_arrayt json_array = get_untyped_array(json, element_type);
  for(auto it = json_array.begin(); it < json_array.end(); it++, index++)
  {
    const dereference_exprt element_at_index = array_element_from_pointer(
      array_init_data, from_integer(index, java_int_type()));
    result.append(
      assign_from_json_rec(element_at_index, *it, inferred_element_type, info));
  }
  return result;
}
 
static std::pair<symbol_exprt, code_with_references_listt>
nondet_length(allocate_objectst &allocate, source_locationt loc)
{
  symbol_exprt length_expr = allocate.allocate_automatic_local_object(
    java_int_type(), "user_specified_array_length");
  code_with_references_listt code;
  code.add(code_frontend_assignt{
    length_expr, side_effect_expr_nondett{java_int_type(), loc}});
  code.add(code_assumet{binary_predicate_exprt{
    length_expr, ID_ge, from_integer(0, java_int_type())}});
  return std::make_pair(length_expr, std::move(code));
}
 
static std::pair<code_with_references_listt, exprt>
assign_det_length_array_from_json(
  const exprt &expr,
  const jsont &json,
  const std::optional<std::string> &type_from_array,
  object_creation_infot &info)
{
  PRECONDITION(is_java_array_type(expr.type()));
  const auto &element_type = java_array_element_type(
    to_struct_tag_type(to_java_reference_type(expr.type()).base_type()));
  const json_arrayt json_array = get_untyped_array(json, element_type);
  const auto number_of_elements =
    from_integer(json_array.size(), java_int_type());
  return {
    assign_array_data_component_from_json(expr, json, type_from_array, info),
    number_of_elements};
}
 
static code_with_references_listt assign_nondet_length_array_from_json(
  const exprt &array,
  const jsont &json,
  const exprt &given_length_expr,
  const std::optional<std::string> &type_from_array,
  object_creation_infot &info)
{
  PRECONDITION(is_java_array_type(array.type()));
  const auto &element_type = java_array_element_type(
    to_struct_tag_type(to_java_reference_type(array.type()).base_type()));
  const json_arrayt json_array = get_untyped_array(json, element_type);
  code_with_references_listt result;
  exprt number_of_elements = from_integer(json_array.size(), java_int_type());
  result.add(code_assumet{and_exprt{
    binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements},
    binary_predicate_exprt{
      given_length_expr,
      ID_le,
      from_integer(info.max_user_array_length, java_int_type())}}});
  result.append(
    assign_array_data_component_from_json(array, json, type_from_array, info));
  return result;
}
 
static code_frontend_assignt assign_string_from_json(
  const jsont &json,
  const exprt &expr,
  object_creation_infot &info)
{
  const auto json_string = get_untyped_string(json);
  PRECONDITION(json_string.is_string());
  return code_frontend_assignt{
    expr,
    get_or_create_string_literal_symbol(
      json_string.value, info.symbol_table, true)};
}
 
static code_with_references_listt assign_struct_components_from_json(
  const exprt &expr,
  const jsont &json,
  object_creation_infot &info)
{
  const java_class_typet &java_class_type =
    to_java_class_type(namespacet{info.symbol_table}.follow(expr.type()));
  code_with_references_listt result;
  for(const auto &component : java_class_type.components())
  {
    const irep_idt &component_name = component.get_name();
    if(
      component_name == JAVA_CLASS_IDENTIFIER_FIELD_NAME ||
      component_name == "cproverMonitorCount")
    {
      continue;
    }
    member_exprt member_expr{expr, component_name, component.type()};
    if(component_name[0] == '@') // component is parent struct type
    {
      result.append(
        assign_struct_components_from_json(member_expr, json, info));
    }
    else // component is class field (pointer to struct)
    {
      const auto member_json = [&]() -> jsont {
        if(
          is_primitive_wrapper_type_id(java_class_type.get_name()) &&
          id2string(component_name) == "value")
        {
          return get_untyped_primitive(json);
        }
        return json[id2string(component_name)];
      }();
      result.append(assign_from_json_rec(member_expr, member_json, {}, info));
    }
  }
  return result;
}
 
static code_with_references_listt assign_struct_from_json(
  const exprt &expr,
  const jsont &json,
  object_creation_infot &info)
{
  const namespacet ns{info.symbol_table};
  const java_class_typet &java_class_type =
    to_java_class_type(ns.follow(expr.type()));
  code_with_references_listt result;
  if(is_java_string_type(java_class_type))
  {
    result.add(assign_string_from_json(json, expr, info));
  }
  else
  {
    auto initial_object = zero_initializer(expr.type(), info.loc, ns);
    CHECK_RETURN(initial_object.has_value());
    set_class_identifier(
      to_struct_expr(*initial_object),
      ns,
      struct_tag_typet("java::" + id2string(java_class_type.get_tag())));
    result.add(code_frontend_assignt{expr, *initial_object});
    result.append(assign_struct_components_from_json(expr, json, info));
  }
  return result;
}
 
static code_with_references_listt assign_non_enum_pointer_from_json(
  const exprt &expr,
  const jsont &json,
  object_creation_infot &info)
{
  code_with_references_listt result;
  code_blockt output_code;
  exprt dereferenced_symbol_expr =
    info.allocate_objects.allocate_dynamic_object(
      output_code, expr, to_pointer_type(expr.type()).base_type());
  for(codet &code : output_code.statements())
    result.add(std::move(code));
  result.append(assign_struct_from_json(dereferenced_symbol_expr, json, info));
  return result;
}
 
static code_with_references_listt assign_enum_from_json(
  const exprt &expr,
  const jsont &json,
  object_creation_infot &info)
{
  const auto &java_class_type = followed_class_type(expr, info.symbol_table);
  const std::string &enum_name = id2string(java_class_type.get_name());
  code_with_references_listt result;
  if(const auto func = info.symbol_table.lookup(clinit_wrapper_name(enum_name)))
    result.add(code_function_callt{func->symbol_expr()});
 
  const irep_idt values_name = enum_name + ".$VALUES";
  if(!info.symbol_table.has_symbol(values_name))
  {
    // Fallback: generate a new enum instance instead of getting it from $VALUES
    result.append(assign_non_enum_pointer_from_json(expr, json, info));
    return result;
  }
 
  dereference_exprt values_struct{
    info.symbol_table.lookup_ref(values_name).symbol_expr()};
  const auto &values_struct_type =
    to_struct_type(namespacet{info.symbol_table}.follow(values_struct.type()));
  PRECONDITION(is_valid_java_array(values_struct_type));
  const member_exprt values_data = member_exprt{
    values_struct, "data", values_struct_type.components()[2].type()};
 
  const exprt ordinal_expr =
    from_integer(std::stoi(json["ordinal"].value), java_int_type());
 
  result.add(code_frontend_assignt{
    expr,
    typecast_exprt::conditional_cast(
      array_element_from_pointer(values_data, ordinal_expr), expr.type())});
  return result;
}
 
static code_with_references_listt assign_pointer_from_json(
  const exprt &expr,
  const jsont &json,
  object_creation_infot &info)
{
  // This check can be removed when tracking reference-equal objects across
  // different classes has been implemented.
  if(has_enum_type(expr, info.symbol_table))
    return assign_enum_from_json(expr, json, info);
  else
    return assign_non_enum_pointer_from_json(expr, json, info);
}
 
static code_with_references_listt assign_pointer_with_given_type_from_json(
  const exprt &expr,
  const jsont &json,
  const java_class_typet &runtime_type,
  object_creation_infot &info)
{
  const auto &pointer_type = to_pointer_type(expr.type());
  pointer_typet replacement_pointer_type =
    pointer_to_replacement_type(pointer_type, runtime_type);
  if(!equal_java_types(pointer_type, replacement_pointer_type))
  {
    const auto &new_symbol =
      info.allocate_objects.allocate_automatic_local_object(
        replacement_pointer_type, "user_specified_subtype_symbol");
    if(info.needed_lazy_methods)
    {
      info.needed_lazy_methods->add_all_needed_classes(
        replacement_pointer_type);
    }
 
    auto result = assign_pointer_from_json(new_symbol, json, info);
    result.add(
      code_frontend_assignt{expr, typecast_exprt{new_symbol, pointer_type}});
    return result;
  }
  else
    return assign_pointer_from_json(expr, json, info);
}
 
struct get_or_create_reference_resultt
{
  bool newly_allocated;
  std::unordered_map<std::string, object_creation_referencet>::iterator
    reference;
  code_with_references_listt code;
};
 
static get_or_create_reference_resultt get_or_create_reference(
  const exprt &expr,
  const std::string &id,
  object_creation_infot &info)
{
  const auto &pointer_type = to_pointer_type(expr.type());
  const auto id_it = info.references.find(id);
  if(id_it == info.references.end())
  {
    code_with_references_listt code;
    object_creation_referencet reference;
    if(is_java_array_type(expr.type()))
    {
      reference.expr = info.allocate_objects.allocate_automatic_local_object(
        pointer_type, "user_specified_array_ref");
      reference.array_length =
        info.allocate_objects.allocate_automatic_local_object(
          java_int_type(), "user_specified_array_length");
      code.add(reference_allocationt{id, info.loc});
    }
    else
    {
      code_blockt block;
      reference.expr = info.allocate_objects.allocate_dynamic_object_symbol(
        block, expr, pointer_type.base_type());
      code.add(block);
    }
    auto iterator_inserted_pair = info.references.insert({id, reference});
    return {iterator_inserted_pair.second, iterator_inserted_pair.first, code};
  }
  return {false, id_it, {}};
}
 
static code_with_references_listt assign_reference_from_json(
  const exprt &expr,
  const jsont &json,
  const std::optional<std::string> &type_from_array,
  object_creation_infot &info)
{
  const std::string &id = has_enum_type(expr, info.symbol_table)
                            ? get_enum_id(expr, json, info.symbol_table)
                            : get_id_or_reference_value(json);
  auto get_reference_result = get_or_create_reference(expr, id, info);
  const bool is_new_id = get_reference_result.newly_allocated;
  object_creation_referencet &reference =
    get_reference_result.reference->second;
  code_with_references_listt result = std::move(get_reference_result.code);
  if(has_id(json) || (is_new_id && has_enum_type(expr, info.symbol_table)))
  {
    if(is_java_array_type(expr.type()))
    {
      INVARIANT(
        reference.array_length, "an array reference should store its length");
      if(has_nondet_length(json))
      {
        result.append(assign_nondet_length_array_from_json(
          reference.expr,
          json,
          *reference.array_length,
          type_from_array,
          info));
      }
      else
      {
        auto code_length_pair = assign_det_length_array_from_json(
          reference.expr, json, type_from_array, info);
        result.append(std::move(code_length_pair.first));
        reference.array_length = std::move(code_length_pair.second);
      }
    }
    else
    {
      result.append(
        assign_struct_from_json(dereference_exprt(reference.expr), json, info));
    }
  }
  result.add(code_frontend_assignt{
    expr, typecast_exprt::conditional_cast(reference.expr, expr.type())});
  return result;
}
 
code_with_references_listt assign_from_json_rec(
  const exprt &expr,
  const jsont &json,
  const std::optional<std::string> &type_from_array,
  object_creation_infot &info)
{
  code_with_references_listt result;
  if(can_cast_type<pointer_typet>(expr.type()))
  {
    if(json.is_null())
    {
      result.add(assign_null(expr));
      return result;
    }
    else if(
      is_reference(json) || has_id(json) ||
      is_enum_with_type_equal_to_declaring_type(
        expr, info.symbol_table, info.declaring_class_type))
    // The last condition can be replaced with
    // has_enum_type(expr, info.symbol_table) once tracking reference-equality
    // across different classes has been implemented.
    {
      return assign_reference_from_json(expr, json, type_from_array, info);
    }
    else if(is_java_array_type(expr.type()))
    {
      if(has_nondet_length(json))
      {
        auto length_code_pair = nondet_length(info.allocate_objects, info.loc);
        length_code_pair.second.add(
          allocate_array(expr, length_code_pair.first, info.loc));
        length_code_pair.second.append(assign_nondet_length_array_from_json(
          expr, json, length_code_pair.first, type_from_array, info));
        return length_code_pair.second;
      }
      else
      {
        PRECONDITION(is_java_array_type(expr.type()));
        const auto &element_type = java_array_element_type(
          to_struct_tag_type(to_java_reference_type(expr.type()).base_type()));
        const std::size_t length = get_untyped_array(json, element_type).size();
        result.add(allocate_array(
          expr, from_integer(length, java_int_type()), info.loc));
        result.append(assign_array_data_component_from_json(
          expr, json, type_from_array, info));
        return result;
      }
    }
    else if(
      const auto runtime_type =
        ::runtime_type(json, type_from_array, info.symbol_table))
    {
      return assign_pointer_with_given_type_from_json(
        expr, json, *runtime_type, info);
    }
    else
      return assign_pointer_from_json(expr, json, info);
  }
  else
    result.append(
      assign_primitive_from_json(expr, get_untyped_primitive(json)));
  return result;
}
 
code_with_references_listt assign_from_json(
  const exprt &expr,
  const jsont &json,
  const irep_idt &function_id,
  symbol_table_baset &symbol_table,
  std::optional<ci_lazy_methods_neededt> &needed_lazy_methods,
  size_t max_user_array_length,
  std::unordered_map<std::string, object_creation_referencet> &references)
{
  source_locationt location{};
  location.set_function(function_id);
  allocate_objectst allocate(ID_java, location, function_id, symbol_table);
  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.");
  const auto &class_type =
    to_java_class_type(symbol_table.lookup_ref(*class_name).type);
  object_creation_infot info{allocate,
                             symbol_table,
                             needed_lazy_methods,
                             references,
                             location,
                             max_user_array_length,
                             class_type};
  code_with_references_listt code_with_references =
    assign_from_json_rec(expr, json, {}, info);
  code_blockt assignments;
  allocate.declare_created_symbols(assignments);
  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;
}