cprover
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 
14 #include <util/c_types.h>
15 
16 bool cpp_typecheckt::find_dtor(const symbolt &symbol) const
17 {
18  const irept &components=
19  symbol.type.find(ID_components);
20 
21  forall_irep(cit, components.get_sub())
22  {
23  if(cit->get(ID_base_name)=="~"+id2string(symbol.base_name))
24  return true;
25  }
26 
27  return false;
28 }
29 
32  const symbolt &symbol,
33  cpp_declarationt &dtor)
34 {
35  assert(symbol.type.id()==ID_struct ||
36  symbol.type.id()==ID_union);
37 
38  irept name;
39  name.id(ID_name);
40  name.set(ID_identifier, "~"+id2string(symbol.base_name));
41  name.set(ID_C_source_location, symbol.location);
42 
43  cpp_declaratort decl;
44  decl.name().id(ID_cpp_name);
45  decl.name().move_to_sub(name);
46  decl.type().id(ID_function_type);
47  decl.type().subtype().make_nil();
48 
49  decl.value().id(ID_code);
50  decl.value().add(ID_type).id(ID_code);
51  decl.value().set(ID_statement, ID_block);
52  decl.add("cv").make_nil();
53  decl.add("throw_decl").make_nil();
54 
55  dtor.add(ID_type).id(ID_destructor);
56  dtor.add(ID_storage_spec).id(ID_cpp_storage_spec);
57  dtor.move_to_operands(decl);
58 }
59 
64 {
65  assert(symbol.type.id()==ID_struct ||
66  symbol.type.id()==ID_union);
67 
68  source_locationt source_location=symbol.type.source_location();
69 
70  source_location.set_function(
71  id2string(symbol.base_name)+
72  "::~"+id2string(symbol.base_name)+"()");
73 
74  code_blockt block;
75 
76  const struct_union_typet::componentst &components =
78 
79  // take care of virtual methods
80  for(struct_union_typet::componentst::const_iterator
81  cit=components.begin();
82  cit!=components.end();
83  cit++)
84  {
85  if(cit->get_bool("is_vtptr"))
86  {
87  exprt name(ID_name);
88  name.set(ID_identifier, cit->get(ID_base_name));
89 
90  cpp_namet cppname;
91  cppname.move_to_sub(name);
92 
93  const symbolt &virtual_table_symbol_type =
94  lookup(cit->type().subtype().get(ID_identifier));
95 
96  const symbolt &virtual_table_symbol_var = lookup(
97  id2string(virtual_table_symbol_type.name) + "@" +
98  id2string(symbol.name));
99 
100  exprt var=virtual_table_symbol_var.symbol_expr();
101  address_of_exprt address(var);
102  assert(address.type()==cit->type());
103 
104  already_typechecked(address);
105 
106  exprt ptrmember(ID_ptrmember);
107  ptrmember.set(ID_component_name, cit->get(ID_name));
108  ptrmember.operands().push_back(exprt("cpp-this"));
109 
110  code_assignt assign(ptrmember, address);
111  block.operands().push_back(assign);
112  continue;
113  }
114  }
115 
116  // call the data member destructors in the reverse order
117  for(struct_union_typet::componentst::const_reverse_iterator
118  cit=components.rbegin();
119  cit!=components.rend();
120  cit++)
121  {
122  const typet &type=cit->type();
123 
124  if(cit->get_bool(ID_from_base) ||
125  cit->get_bool(ID_is_type) ||
126  cit->get_bool(ID_is_static) ||
127  type.id()==ID_code ||
128  is_reference(type) ||
129  cpp_is_pod(type))
130  continue;
131 
132  irept name(ID_name);
133  name.set(ID_identifier, cit->get(ID_base_name));
134  name.set(ID_C_source_location, source_location);
135 
136  cpp_namet cppname;
137  cppname.get_sub().push_back(name);
138 
139  exprt member(ID_ptrmember, type);
140  member.set(ID_component_cpp_name, cppname);
141  member.operands().push_back(
142  symbol_exprt(ID_this, pointer_type(symbol.type)));
143  member.add_source_location() = source_location;
144 
145  const bool disabled_access_control = disable_access_control;
146  disable_access_control = true;
147  codet dtor_code = cpp_destructor(source_location, member);
148  disable_access_control = disabled_access_control;
149 
150  if(dtor_code.is_not_nil())
151  block.move_to_operands(dtor_code);
152  }
153 
154  const irept::subt &bases=symbol.type.find(ID_bases).get_sub();
155 
156  // call the base destructors in the reverse order
157  for(irept::subt::const_reverse_iterator
158  bit=bases.rbegin();
159  bit!=bases.rend();
160  bit++)
161  {
162  assert(bit->id()==ID_base);
163  assert(bit->find(ID_type).id()==ID_symbol);
164  const symbolt &psymb = lookup(bit->find(ID_type).get(ID_identifier));
165 
166  symbol_exprt this_ptr(ID_this, pointer_type(symbol.type));
167  dereference_exprt object(this_ptr, psymb.type);
168  object.add_source_location() = source_location;
169 
170  const bool disabled_access_control = disable_access_control;
171  disable_access_control = true;
172  exprt dtor_code = cpp_destructor(source_location, object);
173  disable_access_control = disabled_access_control;
174 
175  if(dtor_code.is_not_nil())
176  block.move_to_operands(dtor_code);
177  }
178 
179  return block;
180 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
void set_function(const irep_idt &function)
codet dtor(const symbolt &symb)
produces destructor code for a class object
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
std::vector< irept > subt
Definition: irep.h:160
void move_to_sub(irept &irep)
Definition: irep.cpp:204
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
void default_dtor(const symbolt &symb, cpp_declarationt &dtor)
Note:
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
codet cpp_destructor(const source_locationt &source_location, const exprt &object)
subt & get_sub()
Definition: irep.h:317
const irep_idt & id() const
Definition: irep.h:259
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
Operator to dereference a pointer.
Definition: std_expr.h:3282
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
Base class for tree-like data structures with sharing.
Definition: irep.h:156
C++ Language Type Checking.
Operator to return the address of an object.
Definition: std_expr.h:3168
bool find_dtor(const symbolt &symbol) const
const source_locationt & source_location() const
Definition: type.h:97
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
Base class for all expressions.
Definition: expr.h:42
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
irept & add(const irep_namet &name)
Definition: irep.cpp:306
void make_nil()
Definition: irep.h:315
bool disable_access_control
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:89
cpp_namet & name()
Expression to hold a symbol (variable)
Definition: std_expr.h:90
A statement in a programming language.
Definition: std_code.h:21
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
Assignment.
Definition: std_code.h:196
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
#define forall_irep(it, irep)
Definition: irep.h:62