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

Module: C++ Language Type Checking

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

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

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

#include "cpp_typecheck.h"

#include <util/c_types.h>
#include <util/std_expr.h>

void cpp_typecheckt::do_virtual_table(const symbolt &symbol)
{
  assert(symbol.type.id()==ID_struct);

  // builds virtual-table value maps: (class x virtual_name x value)
  std::map<irep_idt, std::map<irep_idt, exprt> > vt_value_maps;

  const struct_typet &struct_type=to_struct_type(symbol.type);

  for(std::size_t i=0; i < struct_type.components().size(); i++)
  {
    const struct_typet::componentt &compo=struct_type.components()[i];
    if(!compo.get_bool(ID_is_virtual))
      continue;

    const code_typet &code_type=to_code_type(compo.type());
    assert(code_type.parameters().size() > 0);

    const pointer_typet &parameter_pointer_type=
      to_pointer_type(code_type.parameters()[0].type());

    const irep_idt &class_id =
      parameter_pointer_type.subtype().get(ID_identifier);

    std::map<irep_idt, exprt> &value_map =
      vt_value_maps[class_id];

    exprt e=symbol_exprt(compo.get_name(), code_type);

    if(compo.get_bool(ID_is_pure_virtual))
    {
      pointer_typet code_pointer_type=pointer_type(code_type);
      e=null_pointer_exprt(code_pointer_type);
      value_map[compo.get(ID_virtual_name)] = e;
    }
    else
    {
      address_of_exprt address(e);
      value_map[compo.get(ID_virtual_name)] = address;
    }
  }

  // create virtual-table symbol variables
  for(std::map<irep_idt, std::map<irep_idt, exprt> >::const_iterator cit =
      vt_value_maps.begin(); cit!=vt_value_maps.end(); cit++)
  {
    const std::map<irep_idt, exprt> &value_map=cit->second;

    const symbolt &late_cast_symb = lookup(cit->first);
    const symbolt &vt_symb_type =
      lookup("virtual_table::" + id2string(late_cast_symb.name));

    symbolt vt_symb_var;
    vt_symb_var.name=
      id2string(vt_symb_type.name) + "@"+ id2string(symbol.name);
    vt_symb_var.base_name=
      id2string(vt_symb_type.base_name) + "@" + id2string(symbol.base_name);
    vt_symb_var.mode = symbol.mode;
    vt_symb_var.module=module;
    vt_symb_var.location=vt_symb_type.location;
    vt_symb_var.type = struct_tag_typet(vt_symb_type.name);
    vt_symb_var.is_lvalue=true;
    vt_symb_var.is_static_lifetime=true;

    // do the values
    const struct_typet &vt_type=to_struct_type(vt_symb_type.type);

    struct_exprt values({}, struct_tag_typet(vt_symb_type.name));

    for(const auto &compo : vt_type.components())
    {
      std::map<irep_idt, exprt>::const_iterator cit2 =
        value_map.find(compo.get_base_name());
      assert(cit2!=value_map.end());
      const exprt &value=cit2->second;
      assert(value.type()==compo.type());
      values.operands().push_back(value);
    }
    vt_symb_var.value=values;

    bool failed=!symbol_table.insert(std::move(vt_symb_var)).second;
    CHECK_RETURN(!failed);
  }
}
