CBMC
cpp_typecheck_destructor.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
15 
16 #include <util/pointer_expr.h>
17 
18 bool cpp_typecheckt::find_dtor(const symbolt &symbol) const
19 {
20  for(const auto &c : to_struct_type(symbol.type).components())
21  {
22  if(c.get_base_name() == "~" + id2string(symbol.base_name))
23  return true;
24  }
25 
26  return false;
27 }
28 
31  const symbolt &symbol,
32  cpp_declarationt &dtor)
33 {
34  assert(symbol.type.id()==ID_struct ||
35  symbol.type.id()==ID_union);
36 
37  cpp_declaratort decl;
38  decl.name() = cpp_namet("~" + id2string(symbol.base_name), symbol.location);
39  decl.type().id(ID_function_type);
40  decl.type().add_subtype().make_nil();
41 
42  decl.value() = code_blockt();
43  decl.add(ID_cv).make_nil();
44  decl.add(ID_throw_decl).make_nil();
45 
46  dtor.add(ID_type).id(ID_destructor);
47  dtor.add(ID_storage_spec).id(ID_cpp_storage_spec);
48  dtor.add_to_operands(std::move(decl));
49 }
50 
52 codet cpp_typecheckt::dtor(const symbolt &symbol, const symbol_exprt &this_expr)
53 {
54  assert(symbol.type.id()==ID_struct ||
55  symbol.type.id()==ID_union);
56 
57  source_locationt source_location=symbol.type.source_location();
58 
59  source_location.set_function(
60  id2string(symbol.base_name)+
61  "::~"+id2string(symbol.base_name)+"()");
62 
63  code_blockt block;
64 
65  const struct_union_typet::componentst &components =
67 
68  // take care of virtual methods
69  for(const auto &c : components)
70  {
71  if(c.get_bool(ID_is_vtptr))
72  {
73  const cpp_namet cppname(c.get_base_name());
74 
75  const symbolt &virtual_table_symbol_type =
76  lookup(to_pointer_type(c.type()).base_type().get(ID_identifier));
77 
78  const symbolt &virtual_table_symbol_var = lookup(
79  id2string(virtual_table_symbol_type.name) + "@" +
80  id2string(symbol.name));
81 
82  exprt var=virtual_table_symbol_var.symbol_expr();
83  address_of_exprt address(var);
84  assert(address.type() == c.type());
85 
87 
88  exprt ptrmember(ID_ptrmember);
89  ptrmember.set(ID_component_name, c.get_name());
90  ptrmember.operands().push_back(this_expr);
91 
92  code_frontend_assignt assign(ptrmember, address);
93  block.add(assign);
94  continue;
95  }
96  }
97 
98  // call the data member destructors in the reverse order
99  for(struct_union_typet::componentst::const_reverse_iterator
100  cit=components.rbegin();
101  cit!=components.rend();
102  cit++)
103  {
104  const typet &type=cit->type();
105 
106  if(cit->get_bool(ID_from_base) ||
107  cit->get_bool(ID_is_type) ||
108  cit->get_bool(ID_is_static) ||
109  type.id()==ID_code ||
110  is_reference(type) ||
111  cpp_is_pod(type))
112  continue;
113 
114  const cpp_namet cppname(cit->get_base_name(), source_location);
115 
116  exprt member(ID_ptrmember, type);
117  member.set(ID_component_cpp_name, cppname);
118  member.operands().push_back(this_expr);
119  member.add_source_location() = source_location;
120 
121  const bool disabled_access_control = disable_access_control;
122  disable_access_control = true;
123  auto dtor_code = cpp_destructor(source_location, member);
124  disable_access_control = disabled_access_control;
125 
126  if(dtor_code.has_value())
127  block.add(dtor_code.value());
128  }
129 
130  if(symbol.type.id() == ID_union)
131  return std::move(block);
132 
133  const auto &bases = to_struct_type(symbol.type).bases();
134 
135  // call the base destructors in the reverse order
136  for(class_typet::basest::const_reverse_iterator bit = bases.rbegin();
137  bit != bases.rend();
138  bit++)
139  {
140  DATA_INVARIANT(bit->id() == ID_base, "base class expression expected");
141  const symbolt &psymb = lookup(bit->type());
142 
143  dereference_exprt object{this_expr, psymb.type};
144  object.add_source_location() = source_location;
145 
146  const bool disabled_access_control = disable_access_control;
147  disable_access_control = true;
148  auto dtor_code = cpp_destructor(source_location, object);
149  disable_access_control = disabled_access_control;
150 
151  if(dtor_code.has_value())
152  block.add(dtor_code.value());
153  }
154 
155  return std::move(block);
156 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:147
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:129
goto_instruction_code.h
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:120
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
irept::make_nil
void make_nil()
Definition: irep.h:454
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:659
cpp_declaratort::name
cpp_namet & name()
Definition: cpp_declarator.h:36
exprt
Base class for all expressions.
Definition: expr.h:55
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:140
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
cpp_typecheckt::dtor
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
Definition: cpp_typecheck_destructor.cpp:52
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
irept::get
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
cpp_typecheckt::default_dtor
void default_dtor(const symbolt &symb, cpp_declarationt &dtor)
Note:
Definition: cpp_typecheck_destructor.cpp:30
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
already_typechecked_exprt::make_already_typechecked
static void make_already_typechecked(exprt &expr)
Definition: c_typecheck_base.h:316
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
irept::set
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
typet::source_location
const source_locationt & source_location() const
Definition: type.h:90
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
struct_typet::bases
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
code_frontend_assignt
A codet representing an assignment in the program.
Definition: std_code.h:23
cpp_declarationt
Definition: cpp_declaration.h:21
irept::id
const irep_idt & id() const
Definition: irep.h:396
code_blockt::add
void add(const codet &code)
Definition: std_code.h:168
typet::add_source_location
source_locationt & add_source_location()
Definition: type.h:95
cpp_typecheck.h
typet::add_subtype
typet & add_subtype()
Definition: type.h:71
source_locationt
Definition: source_location.h:18
cpp_typecheckt::find_dtor
bool find_dtor(const symbolt &symbol) const
Definition: cpp_typecheck_destructor.cpp:18
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:143
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
pointer_typet::base_type
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:162
cpp_declaratort::value
exprt & value()
Definition: cpp_declarator.h:42
exprt::operands
operandst & operands()
Definition: expr.h:94
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:370
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:216
cpp_typecheckt::cpp_destructor
optionalt< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
Definition: cpp_destructor.cpp:19
cpp_namet
Definition: cpp_name.h:16
cpp_typecheckt::disable_access_control
bool disable_access_control
Definition: cpp_typecheck.h:589
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
cpp_declaratort
Definition: cpp_declarator.h:19
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:28