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