/*******************************************************************\

Module: C++ Language Type Checking

Author: Daniel Kroening, kroening@cs.cmu.edu

\*******************************************************************/

/// \file
/// C++ Language Type Checking

#include "cpp_typecheck.h"

#include <util/arith_tools.h>

#include <util/c_types.h>

/// \return typechecked code
std::optional<codet> cpp_typecheckt::cpp_destructor(
  const source_locationt &source_location,
  const exprt &object)
{
  elaborate_class_template(object.type());

  CHECK_RETURN(!is_reference(object.type()));

  // PODs don't need a destructor
  if(cpp_is_pod(object.type()))
    return {};

  if(object.type().id() == ID_array)
  {
    const exprt &size_expr = to_array_type(object.type()).size();

    if(size_expr.id() == ID_infinity)
      return {}; // don't initialize

    exprt tmp_size=size_expr;
    make_constant_index(tmp_size);

    mp_integer s;
    if(to_integer(to_constant_expr(tmp_size), s))
    {
      error().source_location=source_location;
      error() << "array size '" << to_string(size_expr) << "' is not a constant"
              << eom;
      throw 0;
    }

    code_blockt new_code;
    new_code.add_source_location()=source_location;

    // for each element of the array, call the destructor
    for(mp_integer i=0; i < s; ++i)
    {
      exprt constant = from_integer(i, c_index_type());
      constant.add_source_location()=source_location;

      index_exprt index(object, constant);
      index.add_source_location()=source_location;

      auto i_code = cpp_destructor(source_location, index);
      if(i_code.has_value())
        new_code.add_to_operands(std::move(i_code.value()));
    }

    return std::move(new_code);
  }
  else
  {
    const struct_typet &struct_type =
      follow_tag(to_struct_tag_type(object.type()));

    // enter struct scope
    cpp_save_scopet save_scope(cpp_scopes);
    cpp_scopes.set_scope(struct_type.get(ID_name));

    // find name of destructor
    const struct_typet::componentst &components=
      struct_type.components();

    irep_idt dtor_name;

    for(const auto &c : components)
    {
      const typet &type = c.type();

      if(
        !c.get_bool(ID_from_base) && type.id() == ID_code &&
        to_code_type(type).return_type().id() == ID_destructor)
      {
        dtor_name = c.get_base_name();
        break;
      }
    }

    INVARIANT(!dtor_name.empty(), "non-PODs should have a destructor");

    cpp_namet cpp_name(dtor_name, source_location);

    exprt member(ID_member);
    member.add(ID_component_cpp_name) = cpp_name;
    member.copy_to_operands(object);

    side_effect_expr_function_callt function_call(
      std::move(member), {}, uninitialized_typet{}, source_location);

    typecheck_side_effect_function_call(function_call);
    already_typechecked_exprt::make_already_typechecked(function_call);

    code_expressiont new_code(function_call);
    new_code.add_source_location() = source_location;

    return std::move(new_code);
  }
}