cpp_typecheck.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: C++ Language Type Checking
 
Author: Daniel Kroening, kroening@cs.cmu.edu
 
\*******************************************************************/
 
 
#include "cpp_typecheck.h"
 
#include <util/pointer_expr.h>
#include <util/source_location.h>
#include <util/symbol_table.h>
 
#include <ansi-c/builtin_factory.h>
#include <ansi-c/gcc_version.h>
 
#include "cpp_declarator.h"
#include "cpp_util.h"
#include "expr2cpp.h"
 
cpp_typecheckt::cpp_typecheckt(
  cpp_parse_treet &_cpp_parse_tree,
  symbol_table_baset &_symbol_table,
  const std::string &_module,
  message_handlert &message_handler)
  : c_typecheck_baset(_symbol_table, _module, message_handler),
    cpp_parse_tree(_cpp_parse_tree),
    template_counter(0),
    anon_counter(0),
    disable_access_control(false),
    support_float16_type(false)
{
  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
  {
    gcc_versiont gcc_version;
    gcc_version.get("gcc");
    if(
      gcc_version.flavor == gcc_versiont::flavort::GCC &&
      gcc_version.is_at_least(13u))
    {
      support_float16_type = true;
    }
  }
}
cpp_typecheckt::cpp_typecheckt( {…}
 
cpp_typecheckt::cpp_typecheckt(
  cpp_parse_treet &_cpp_parse_tree,
  symbol_table_baset &_symbol_table1,
  const symbol_table_baset &_symbol_table2,
  const std::string &_module,
  message_handlert &message_handler)
  : c_typecheck_baset(_symbol_table1, _symbol_table2, _module, message_handler),
    cpp_parse_tree(_cpp_parse_tree),
    template_counter(0),
    anon_counter(0),
    disable_access_control(false),
    support_float16_type(false)
{
  if(config.ansi_c.preprocessor == configt::ansi_ct::preprocessort::GCC)
  {
    gcc_versiont gcc_version;
    gcc_version.get("gcc");
    if(
      gcc_version.flavor == gcc_versiont::flavort::GCC &&
      gcc_version.is_at_least(13u))
    {
      support_float16_type = true;
    }
  }
}
cpp_typecheckt::cpp_typecheckt( {…}
 
void cpp_typecheckt::convert(cpp_itemt &item)
{
  if(item.is_declaration())
    convert(to_cpp_declaration(item));
  else if(item.is_linkage_spec())
    convert(item.get_linkage_spec());
  else if(item.is_namespace_spec())
    convert(item.get_namespace_spec());
  else if(item.is_using())
    convert(item.get_using());
  else if(item.is_static_assert())
    convert(item.get_static_assert());
  else
  {
    error().source_location=item.source_location();
    error() << "unknown parse-tree element: " << item.id() << eom;
    throw 0;
  }
}
void cpp_typecheckt::convert(cpp_itemt &item) {…}
 
void cpp_typecheckt::typecheck()
{
  // default linkage is "automatic"
  current_linkage_spec=ID_auto;
 
  for(auto &item : cpp_parse_tree.items)
    convert(item);
 
  static_and_dynamic_initialization();
 
  typecheck_method_bodies();
 
  do_not_typechecked();
 
  clean_up();
}
void cpp_typecheckt::typecheck() {…}
 
const struct_typet &cpp_typecheckt::this_struct_type()
{
  const exprt &this_expr=
    cpp_scopes.current_scope().this_expr;
 
  CHECK_RETURN(this_expr.is_not_nil());
  CHECK_RETURN(this_expr.type().id() == ID_pointer);
 
  const typet &t = to_pointer_type(this_expr.type()).base_type();
  CHECK_RETURN(t.id() == ID_struct_tag);
  return follow_tag(to_struct_tag_type(t));
}
const struct_typet &cpp_typecheckt::this_struct_type() {…}
 
std::string cpp_typecheckt::to_string(const exprt &expr)
{
  return expr2cpp(expr, *this);
}
std::string cpp_typecheckt::to_string(const exprt &expr) {…}
 
std::string cpp_typecheckt::to_string(const typet &type)
{
  return type2cpp(type, *this);
}
std::string cpp_typecheckt::to_string(const typet &type) {…}
 
bool cpp_typecheck(
  cpp_parse_treet &cpp_parse_tree,
  symbol_table_baset &symbol_table,
  const std::string &module,
  message_handlert &message_handler)
{
  cpp_typecheckt cpp_typecheck(
    cpp_parse_tree, symbol_table, module, message_handler);
  return cpp_typecheck.typecheck_main();
}
bool cpp_typecheck( {…}
 
bool cpp_typecheck(
  exprt &expr,
  message_handlert &message_handler,
  const namespacet &ns)
{
  const unsigned errors_before=
    message_handler.get_message_count(messaget::M_ERROR);
 
  symbol_tablet symbol_table;
  cpp_parse_treet cpp_parse_tree;
 
  cpp_typecheckt cpp_typecheck(cpp_parse_tree, symbol_table,
                               ns.get_symbol_table(), "", message_handler);
 
  try
  {
    cpp_typecheck.typecheck_expr(expr);
  }
 
  catch(int)
  {
    cpp_typecheck.error();
  }
 
  catch(const char *e)
  {
    cpp_typecheck.error() << e << messaget::eom;
  }
 
  catch(const std::string &e)
  {
    cpp_typecheck.error() << e << messaget::eom;
  }
 
  catch(const invalid_source_file_exceptiont &e)
  {
    cpp_typecheck.error().source_location = e.get_source_location();
    cpp_typecheck.error() << e.get_reason() << messaget::eom;
  }
 
  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
}
bool cpp_typecheck( {…}
 
void cpp_typecheckt::static_and_dynamic_initialization()
{
  code_blockt init_block; // Dynamic Initialization Block
 
  disable_access_control = true;
 
  for(const irep_idt &d_it : dynamic_initializations)
  {
    symbolt &symbol = symbol_table.get_writeable_ref(d_it);
 
    if(symbol.is_extern)
      continue;
 
    // PODs are always statically initialized
    if(cpp_is_pod(symbol.type))
      continue;
 
    DATA_INVARIANT(symbol.is_static_lifetime, "should be static");
    DATA_INVARIANT(!symbol.is_type, "should not be a type");
    DATA_INVARIANT(symbol.type.id() != ID_code, "should not be code");
 
    exprt symbol_expr=cpp_symbol_expr(symbol);
 
    // initializer given?
    if(symbol.value.is_not_nil())
    {
      // This will be a constructor call,
      // which we execute.
      init_block.add(to_code(symbol.value));
 
      // Make it nil to get zero initialization by
      // __CPROVER_initialize
      symbol.value.make_nil();
    }
    else
    {
      // use default constructor
      exprt::operandst ops;
 
      auto call = cpp_constructor(symbol.location, symbol_expr, ops);
 
      if(call.has_value())
        init_block.add(call.value());
    }
  }
 
  dynamic_initializations.clear();
 
  // Create the dynamic initialization procedure
  symbolt init_symbol{
    "#cpp_dynamic_initialization#" + id2string(module),
    code_typet({}, typet(ID_constructor)),
    ID_cpp};
  init_symbol.base_name="#cpp_dynamic_initialization#"+id2string(module);
  init_symbol.value.swap(init_block);
  init_symbol.module=module;
 
  symbol_table.insert(std::move(init_symbol));
 
  disable_access_control=false;
}
void cpp_typecheckt::static_and_dynamic_initialization() {…}
 
void cpp_typecheckt::do_not_typechecked()
{
  bool cont;
 
  do
  {
    cont = false;
 
    for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
    {
      const symbolt &symbol = it->second;
 
      if(
        symbol.value.id() == ID_cpp_not_typechecked &&
        symbol.value.get_bool(ID_is_used))
      {
        DATA_INVARIANT(symbol.type.id() == ID_code, "must be code");
        exprt value = symbol.value;
 
        if(symbol.base_name=="operator=")
        {
          cpp_declaratort declarator;
          declarator.add_source_location() = symbol.location;
          default_assignop_value(
            lookup(symbol.type.get(ID_C_member_name)), declarator);
          value.swap(declarator.value());
          cont=true;
        }
        else if(symbol.value.operands().size()==1)
        {
          value = to_unary_expr(symbol.value).op();
          cont=true;
        }
        else
          UNREACHABLE; // Don't know what to do!
 
        symbolt &writable_symbol = it.get_writeable_symbol();
        writable_symbol.value.swap(value);
        convert_function(writable_symbol);
      }
    }
  }
  while(cont);
 
  for(auto it = symbol_table.begin(); it != symbol_table.end(); ++it)
  {
    if(it->second.value.id() == ID_cpp_not_typechecked)
      it.get_writeable_symbol().value.make_nil();
  }
}
void cpp_typecheckt::do_not_typechecked() {…}
 
void cpp_typecheckt::clean_up()
{
  auto it = symbol_table.begin();
 
  while(it != symbol_table.end())
  {
    auto cur_it = it;
    it++;
 
    const symbolt &symbol=cur_it->second;
 
    // erase templates and all member functions that have not been converted
    if(
      symbol.type.get_bool(ID_is_template) ||
      deferred_typechecking.find(symbol.name) != deferred_typechecking.end())
    {
      symbol_table.erase(cur_it);
      continue;
    }
    else if(symbol.type.id()==ID_struct ||
            symbol.type.id()==ID_union)
    {
      // remove methods from 'components'
      struct_union_typet &struct_union_type =
        to_struct_union_type(cur_it.get_writeable_symbol().type);
 
      const struct_union_typet::componentst &components=
        struct_union_type.components();
 
      struct_union_typet::componentst data_members;
      data_members.reserve(components.size());
 
      struct_union_typet::componentst &function_members=
        (struct_union_typet::componentst &)
        (struct_union_type.add(ID_methods).get_sub());
 
      function_members.reserve(components.size());
 
      for(const auto &compo_it : components)
      {
        if(compo_it.get_bool(ID_is_static) ||
           compo_it.get_bool(ID_is_type))
        {
          // skip it
        }
        else if(compo_it.type().id()==ID_code)
        {
          function_members.push_back(compo_it);
        }
        else
        {
          data_members.push_back(compo_it);
        }
      }
 
      struct_union_type.components().swap(data_members);
    }
  }
}
void cpp_typecheckt::clean_up() {…}
 
bool cpp_typecheckt::builtin_factory(const irep_idt &identifier)
{
  return ::builtin_factory(
    identifier, support_float16_type, symbol_table, get_message_handler());
}
bool cpp_typecheckt::builtin_factory(const irep_idt &identifier) {…}
 
bool cpp_typecheckt::contains_cpp_name(const exprt &expr)
{
  if(expr.id() == ID_cpp_name || expr.id() == ID_cpp_declaration)
    return true;
 
  for(const exprt &op : expr.operands())
  {
    if(contains_cpp_name(op))
      return true;
  }
  return false;
}
bool cpp_typecheckt::contains_cpp_name(const exprt &expr) {…}