/*******************************************************************\
Module: C++ Language Type Checking
Author: Daniel Kroening, [email protected]
\*******************************************************************/
/// \file
/// C++ Language Type Checking
#include "cpp_typecheck.h"
#include
#include
#include
#include
#include
#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_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;
}
}
}
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;
}
}
/// typechecking main method
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();
}
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));
}
std::string cpp_typecheckt::to_string(const exprt &expr)
{
return expr2cpp(expr, *this);
}
std::string cpp_typecheckt::to_string(const typet &type)
{
return type2cpp(type, *this);
}
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(
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;
}
/// Initialization of static objects:
///
/// "Objects with static storage duration (3.7.1) shall be zero-initialized
/// (8.5) before any other initialization takes place. Zero-initialization
/// and initialization with a constant expression are collectively called
/// static initialization; all other initialization is dynamic
/// initialization. Objects of POD types (3.9) with static storage duration
/// initialized with constant expressions (5.19) shall be initialized before
/// any dynamic initialization takes place. Objects with static storage
/// duration defined in namespace scope in the same translation unit and
/// dynamically initialized shall be initialized in the order in which their
/// definition appears in the translation unit. [Note: 8.5.1 describes the
/// order in which aggregate members are initialized. The initialization
/// of local static objects is described in 6.7. ]"
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::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::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);
}
}
}
bool cpp_typecheckt::builtin_factory(const irep_idt &identifier)
{
return ::builtin_factory(
identifier, support_float16_type, symbol_table, get_message_handler());
}
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;
}