cpp_typecheck.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: C++ Language Type Checking
 
Author: Daniel Kroening, kroening@cs.cmu.edu
 
\*******************************************************************/
 
 
#ifndef CPROVER_CPP_CPP_TYPECHECK_H
#define CPROVER_CPP_CPP_TYPECHECK_H
 
#include <util/std_code_base.h>
 
#include <ansi-c/c_typecheck_base.h>
 
#include "cpp_parse_tree.h"
#include "cpp_scopes.h"
#include "cpp_typecheck_resolve.h"
#include "template_map.h"
 
#include <list>
#include <set>
#include <unordered_set>
 
class pointer_typet;
class reference_typet;
 
bool cpp_typecheck(
  cpp_parse_treet &cpp_parse_tree,
  symbol_table_baset &symbol_table,
  const std::string &module,
  message_handlert &message_handler);
 
bool cpp_typecheck(
  exprt &expr,
  message_handlert &message_handler,
  const namespacet &ns);
 
class cpp_typecheckt:public c_typecheck_baset
{
public:
  cpp_typecheckt(
    cpp_parse_treet &_cpp_parse_tree,
    symbol_table_baset &_symbol_table,
    const std::string &_module,
    message_handlert &message_handler);
 
  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);
 
  ~cpp_typecheckt() override
  {
  }
  ~cpp_typecheckt() override {…}
 
  void typecheck() override;
 
  // overload to use C++ syntax
  std::string to_string(const typet &) override;
  std::string to_string(const exprt &) override;
 
  friend class cpp_typecheck_resolvet;
  friend class cpp_declarator_convertert;
 
  exprt resolve(
    const cpp_namet &cpp_name,
    const cpp_typecheck_resolvet::wantt want,
    const cpp_typecheck_fargst &fargs,
    bool fail_with_exception=true)
  {
    cpp_typecheck_resolvet cpp_typecheck_resolve(*this);
    return cpp_typecheck_resolve.resolve(
      cpp_name, want, fargs, fail_with_exception);
  }
  exprt resolve( {…}
 
  void typecheck_expr(exprt &) override;
 
  bool cpp_is_pod(const typet &type) const;
 
  std::optional<codet> cpp_constructor(
    const source_locationt &source_location,
    const exprt &object,
    const exprt::operandst &operands);
 
protected:
  cpp_scopest cpp_scopes;
 
  cpp_parse_treet &cpp_parse_tree;
  irep_idt current_linkage_spec;
 
  void convert(cpp_linkage_spect &);
  void convert(cpp_namespace_spect &);
  void convert(cpp_usingt &);
  void convert(cpp_itemt &);
  void convert(cpp_declarationt &);
  void convert(cpp_declaratort &);
  void convert(cpp_static_assertt &);
 
  void convert_initializer(symbolt &symbol);
  void convert_function(symbolt &symbol);
 
  void convert_pmop(exprt &expr);
 
  codet convert_anonymous_union(cpp_declarationt &declaration);
 
  void convert_anon_struct_union_member(
    const cpp_declarationt &declaration,
    const irep_idt &access,
    struct_typet::componentst &components);
 
  //
  // Templates
  //
  void salvage_default_arguments(
    const template_typet &old_type,
    template_typet &new_type);
 
  void convert_template_declaration(cpp_declarationt &declaration);
 
  void convert_non_template_declaration(cpp_declarationt &declaration);
 
  void convert_template_function_or_member_specialization(
    cpp_declarationt &declaration);
 
  void convert_class_template_specialization(
    cpp_declarationt &declaration);
 
  void typecheck_class_template(cpp_declarationt &declaration);
 
  void typecheck_function_template(cpp_declarationt &declaration);
 
  void typecheck_class_template_member(cpp_declarationt &declaration);
 
  std::string class_template_identifier(
    const irep_idt &base_name,
    const template_typet &template_type,
    const cpp_template_args_non_tct &partial_specialization_args);
 
  std::string function_template_identifier(
    const irep_idt &base_name,
    const template_typet &template_type,
    const typet &function_type);
 
  cpp_template_args_tct typecheck_template_args(
    const source_locationt &source_location,
    const symbolt &template_symbol,
    const cpp_template_args_non_tct &template_args);
 
  // template instantiations
  class instantiationt
  {
  public:
    source_locationt source_location;
    irep_idt identifier;
    cpp_template_args_tct full_template_args;
  };
  class instantiationt {…};
 
  typedef std::list<instantiationt> instantiation_stackt;
  instantiation_stackt instantiation_stack;
 
  void show_instantiation_stack(std::ostream &);
 
  class instantiation_levelt
  {
  public:
    instantiation_levelt(
      instantiation_stackt &_instantiation_stack):
      instantiation_stack(_instantiation_stack)
    {
      instantiation_stack.push_back(instantiationt());
    }
    instantiation_levelt( {…}
 
    ~instantiation_levelt()
    {
      instantiation_stack.pop_back();
    }
    ~instantiation_levelt() {…}
 
  private:
    instantiation_stackt &instantiation_stack;
  };
  class instantiation_levelt {…};
 
  const symbolt &class_template_symbol(
    const source_locationt &source_location,
    const symbolt &template_symbol,
    const cpp_template_args_tct &specialization_template_args,
    const cpp_template_args_tct &full_template_args);
 
  void elaborate_class_template(
    const typet &type);
 
  const symbolt &instantiate_template(
    const source_locationt &source_location,
    const symbolt &symbol,
    const cpp_template_args_tct &specialization_template_args,
    const cpp_template_args_tct &full_template_args,
    const typet &specialization = uninitialized_typet{});
 
  void elaborate_class_template(
    const source_locationt &source_location,
    const struct_tag_typet &type);
 
  unsigned template_counter;
  unsigned anon_counter;
 
  template_mapt template_map;
 
  std::string template_suffix(
    const cpp_template_args_tct &template_args);
 
  cpp_scopet &sub_scope_for_instantiation(
    cpp_scopet &template_scope,
    const std::string &suffix);
 
  void
  convert_parameters(const irep_idt &current_mode, code_typet &function_type);
 
  void convert_parameter(
    const irep_idt &current_mode,
    code_typet::parametert &parameter);
 
  //
  // Misc
  //
 
  void default_ctor(
    const source_locationt &source_location,
    const irep_idt &base_name,
    cpp_declarationt &ctor) const;
 
  void default_cpctor(
    const symbolt&, cpp_declarationt &cpctor) const;
 
  void default_assignop(
      const symbolt &symbol, cpp_declarationt &cpctor);
 
  void default_assignop_value(
      const symbolt &symbol, cpp_declaratort &declarator);
 
  void default_dtor(const symbolt &symb, cpp_declarationt &dtor);
 
  codet dtor(const symbolt &symb, const symbol_exprt &this_expr);
 
  void check_member_initializers(
    const struct_typet::basest &bases,
    const struct_typet::componentst &components,
    const irept &initializers);
 
  bool check_component_access(
    const struct_union_typet::componentt &component,
    const struct_union_typet &struct_union_type);
 
  void full_member_initialization(
    const struct_union_typet &struct_union_type,
    irept &initializers);
 
  bool find_cpctor(const symbolt &symbol)const;
  bool find_assignop(const symbolt &symbol)const;
  bool find_dtor(const symbolt &symbol)const;
 
  bool find_parent(
    const symbolt &symb,
    const irep_idt &base_name,
    irep_idt &identifier);
 
  bool get_component(
    const source_locationt &source_location,
    const exprt &object,
    const irep_idt &component_name,
    exprt &member);
 
  void new_temporary(const source_locationt &source_location,
                     const typet &,
                     const exprt::operandst &ops,
                     exprt &temporary);
 
  void new_temporary(const source_locationt &source_location,
                     const typet &,
                     const exprt &op,
                     exprt &temporary);
 
  void static_and_dynamic_initialization();
  void do_not_typechecked();
  void clean_up();
 
  void add_base_components(
        const struct_typet &from,
        const irep_idt &access,
        struct_typet &to,
        std::set<irep_idt> &bases,
        std::set<irep_idt> &vbases,
        bool is_virtual);
 
  bool cast_away_constness(const typet &t1,
                           const typet &t2) const;
 
  void do_virtual_table(const symbolt &symbol);
 
  // we need to be able to delay the typechecking
  // of method bodies to handle methods with
  // bodies in the class definition
  struct method_bodyt
  {
  public:
    method_bodyt(
      symbolt *_method_symbol,
      const template_mapt &_template_map,
      const instantiation_stackt &_instantiation_stack):
      method_symbol(_method_symbol),
      template_map(_template_map),
      instantiation_stack(_instantiation_stack)
    {
    }
    method_bodyt( {…}
 
    symbolt *method_symbol;
    template_mapt template_map;
    instantiation_stackt instantiation_stack;
  };
  struct method_bodyt {…};
 
  typedef std::list<method_bodyt> method_bodiest;
  std::set<irep_idt> methods_seen;
  method_bodiest method_bodies;
 
  void add_method_body(symbolt *_method_symbol);
 
  bool builtin_factory(const irep_idt &) override;
 
  // types
 
  void typecheck_type(typet &) override;
 
  cpp_scopet &typecheck_template_parameters(
    template_typet &type);
 
  void typecheck_compound_type(struct_union_typet &) override;
  void check_fixed_size_array(typet &type);
  void typecheck_enum_type(typet &type);
 
  // determine the scope into which a tag goes
  // (enums, structs, union, classes)
  cpp_scopet &tag_scope(
    const irep_idt &_base_name,
    bool has_body,
    bool tag_only_declaration);
 
  void typecheck_compound_declarator(
    const symbolt &symbol,
    const cpp_declarationt &declaration,
    cpp_declaratort &declarator,
    struct_typet::componentst &components,
    const irep_idt &access,
    bool is_static,
    bool is_typedef,
    bool is_mutable);
 
  void typecheck_friend_declaration(
    symbolt &symbol,
    cpp_declarationt &cpp_declaration);
 
  void put_compound_into_scope(const struct_union_typet::componentt &component);
  void typecheck_compound_body(symbolt &symbol);
  void typecheck_compound_body(struct_union_typet &) override
  {
    UNREACHABLE;
  }
  void typecheck_compound_body(struct_union_typet &) override {…}
  void typecheck_enum_body(symbolt &symbol);
  void typecheck_method_bodies();
  void typecheck_compound_bases(struct_typet &type);
  void add_anonymous_members_to_scope(const symbolt &struct_union_symbol);
 
  void move_member_initializers(
    irept &initializers,
    const code_typet &type,
    exprt &value);
 
  static bool has_const(const typet &type);
  static bool has_volatile(const typet &type);
  static bool has_auto(const typet &type);
 
  void typecheck_member_function(
    const symbolt &compound_symbol,
    struct_typet::componentt &component,
    irept &initializers,
    const typet &method_qualifier,
    exprt &value);
 
  void add_this_to_method_type(
    const symbolt &compound_symbol,
    code_typet &method_type,
    const typet &method_qualifier);
 
  // for function overloading
  irep_idt function_identifier(const typet &type);
 
  void zero_initializer(
    const exprt &object,
    const typet &type,
    const source_locationt &source_location,
    exprt::operandst &ops);
 
  // code conversion
  void typecheck_code(codet &) override;
  void typecheck_try_catch(codet &);
  void typecheck_member_initializer(codet &);
  void typecheck_decl(codet &) override;
  void typecheck_block(code_blockt &) override;
  void typecheck_ifthenelse(code_ifthenelset &) override;
  void typecheck_while(code_whilet &) override;
  void typecheck_switch(codet &) override;
 
  const struct_typet &this_struct_type();
 
  std::optional<codet>
  cpp_destructor(const source_locationt &source_location, const exprt &object);
 
  // expressions
  void explicit_typecast_ambiguity(exprt &);
  void typecheck_expr_main(exprt &) override;
  void typecheck_expr_member(exprt &) override;
  void typecheck_expr_ptrmember(exprt &) override;
  void typecheck_expr_throw(exprt &);
  void typecheck_function_expr(exprt &, const cpp_typecheck_fargst &);
  void typecheck_expr_cpp_name(exprt &, const cpp_typecheck_fargst &);
  void typecheck_expr_member(exprt &, const cpp_typecheck_fargst &);
  void typecheck_expr_ptrmember(exprt &, const cpp_typecheck_fargst &);
  void typecheck_cast_expr(exprt &);
  void typecheck_expr_trinary(if_exprt &) override;
  void typecheck_expr_binary_arithmetic(exprt &) override;
  void typecheck_expr_explicit_typecast(exprt &);
  void typecheck_expr_explicit_constructor_call(exprt &);
  void typecheck_expr_address_of(exprt &) override;
  void typecheck_expr_dereference(exprt &) override;
  void typecheck_expr_function_identifier(exprt &) override;
  void typecheck_expr_reference_to(exprt &);
  void typecheck_expr_this(exprt &);
  void typecheck_expr_new(exprt &);
  void typecheck_expr_sizeof(exprt &) override;
  void typecheck_expr_delete(exprt &);
  void typecheck_expr_side_effect(side_effect_exprt &) override;
  void typecheck_side_effect_assignment(side_effect_exprt &) override;
  void typecheck_side_effect_inc_dec(side_effect_exprt &);
  void typecheck_expr_typecast(exprt &) override;
  void typecheck_expr_index(exprt &) override;
  void typecheck_expr_rel(binary_relation_exprt &) override;
  void typecheck_expr_comma(exprt &) override;
 
  void
  typecheck_function_call_arguments(side_effect_expr_function_callt &) override;
 
  bool operator_is_overloaded(exprt &);
  bool overloadable(const exprt &);
 
  void add_implicit_dereference(exprt &);
 
  void typecheck_side_effect_function_call(
    side_effect_expr_function_callt &) override;
 
  void typecheck_method_application(side_effect_expr_function_callt &);
 
public:
  //
  // Type Conversions
  //
 
  bool standard_conversion_lvalue_to_rvalue(
    const exprt &expr, exprt &new_expr) const;
 
  bool standard_conversion_array_to_pointer(
    const exprt &expr, exprt &new_expr) const;
 
  bool standard_conversion_function_to_pointer(
    const exprt &expr, exprt &new_expr) const;
 
  bool standard_conversion_qualification(
    const exprt &expr, const typet&, exprt &new_expr) const;
 
  bool standard_conversion_integral_promotion(
    const exprt &expr, exprt &new_expr) const;
 
  bool standard_conversion_floating_point_promotion(
    const exprt &expr, exprt &new_expr) const;
 
  bool standard_conversion_integral_conversion(
    const exprt &expr, const typet &type, exprt &new_expr) const;
 
  bool standard_conversion_floating_integral_conversion(
    const exprt &expr, const typet &type, exprt &new_expr) const;
 
  bool standard_conversion_floating_point_conversion(
    const exprt &expr, const typet &type, exprt &new_expr) const;
 
  bool standard_conversion_pointer(
    const exprt &expr, const typet &type, exprt &new_expr);
 
  bool standard_conversion_pointer_to_member(
    const exprt &expr, const typet &type, exprt &new_expr);
 
  bool standard_conversion_boolean(
    const exprt &expr, exprt &new_expr) const;
 
  bool standard_conversion_sequence(
    const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
 
  bool user_defined_conversion_sequence(
    const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
 
  bool reference_related(const exprt &expr, const reference_typet &type) const;
 
  bool reference_compatible(
    const exprt &expr,
    const reference_typet &type,
    unsigned &rank) const;
 
  bool reference_binding(
    exprt expr,
    const reference_typet &type,
    exprt &new_expr,
    unsigned &rank);
 
  bool implicit_conversion_sequence(
    const exprt &expr, const typet &type, exprt &new_expr, unsigned &rank);
 
  bool implicit_conversion_sequence(
    const exprt &expr, const typet &type, unsigned &rank);
 
  bool implicit_conversion_sequence(
    const exprt &expr, const typet &type, exprt &new_expr);
 
  void reference_initializer(exprt &expr, const reference_typet &type);
 
  void implicit_typecast(exprt &expr, const typet &type) override;
 
  void get_bases(const struct_typet &type,
     std::set<irep_idt> &set_bases) const;
 
  void get_virtual_bases(const struct_typet &type,
     std::list<irep_idt> &vbases) const;
 
  bool subtype_typecast(
    const struct_typet &from,
    const struct_typet &to) const;
 
  void make_ptr_typecast(exprt &expr, const pointer_typet &dest_type);
 
  // the C++ typecasts
 
  bool const_typecast(
    const exprt &expr,
    const typet &type,
    exprt &new_expr);
 
  bool dynamic_typecast(
    const exprt &expr,
    const typet &type,
    exprt &new_expr);
 
  bool reinterpret_typecast(
    const exprt &expr,
    const typet &type,
    exprt &new_expr,
    bool check_constantness=true);
 
  bool static_typecast(
    const exprt &expr,
    const typet &type,
    exprt &new_expr,
    bool check_constantness=true);
 
  bool contains_cpp_name(const exprt &);
 
private:
  typedef std::list<irep_idt> dynamic_initializationst;
  dynamic_initializationst dynamic_initializations;
  bool disable_access_control;           // Disable protect and private
  std::unordered_set<irep_idt> deferred_typechecking;
  bool support_float16_type;
};
class cpp_typecheckt:public c_typecheck_baset {…};
 
#endif // CPROVER_CPP_CPP_TYPECHECK_H