cprover
cpp_typecheck_destructor.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: Daniel Kroening, kroening@cs.cmu.edu
6
7\*******************************************************************/
8
11
12#include "cpp_typecheck.h"
13
15
16#include <util/pointer_expr.h>
17
18bool 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().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
52codet 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;
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;
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}
Operator to return the address of an object.
Definition: pointer_expr.h:361
static void make_already_typechecked(exprt &expr)
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
A codet representing an assignment in the program.
Definition: std_code.h:24
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
cpp_namet & name()
optionalt< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
void default_dtor(const symbolt &symb, cpp_declarationt &dtor)
Note:
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
codet dtor(const symbolt &symb, const symbol_exprt &this_expr)
produces destructor code for a class object
bool disable_access_control
bool find_dtor(const symbolt &symbol) const
Operator to dereference a pointer.
Definition: pointer_expr.h:648
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
source_locationt & add_source_location()
Definition: expr.h:235
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
void make_nil()
Definition: irep.h:454
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
void set_function(const irep_idt &function)
const basest & bases() const
Get the collection of base classes/structs.
Definition: std_types.h:262
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
const source_locationt & source_location() const
Definition: type.h:74
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:137
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214