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  lookup(cit->type().subtype().get(ID_identifier));
93 
94  const symbolt &virtual_table_symbol_var = lookup(
95  id2string(virtual_table_symbol_type.name) + "@" +
96  id2string(symbol.name));
97 
98  exprt var=virtual_table_symbol_var.symbol_expr();
99  address_of_exprt address(var);
100  assert(address.type()==cit->type());
101 
102  already_typechecked(address);
103 
104  exprt ptrmember(ID_ptrmember);
105  ptrmember.set(ID_component_name, cit->get(ID_name));
106  ptrmember.operands().push_back(exprt("cpp-this"));
107 
108  code_assignt assign(ptrmember, address);
109  block.operands().push_back(assign);
110  continue;
111  }
112  }
113 
114  // call the data member destructors in the reverse order
115  for(struct_union_typet::componentst::const_reverse_iterator
116  cit=components.rbegin();
117  cit!=components.rend();
118  cit++)
119  {
120  const typet &type=cit->type();
121 
122  if(cit->get_bool(ID_from_base) ||
123  cit->get_bool(ID_is_type) ||
124  cit->get_bool(ID_is_static) ||
125  type.id()==ID_code ||
126  is_reference(type) ||
127  cpp_is_pod(type))
128  continue;
129 
130  irept name(ID_name);
131  name.set(ID_identifier, cit->get(ID_base_name));
132  name.set(ID_C_source_location, source_location);
133 
134  cpp_namet cppname;
135  cppname.get_sub().push_back(name);
136 
137  exprt member(ID_ptrmember);
138  member.set(ID_component_cpp_name, cppname);
139  member.operands().push_back(exprt("cpp-this"));
140  member.add_source_location() = source_location;
141 
142  codet dtor_code=
143  cpp_destructor(source_location, cit->type(), member);
144 
145  if(dtor_code.is_not_nil())
146  block.move_to_operands(dtor_code);
147  }
148 
149  const irept::subt &bases=symbol.type.find(ID_bases).get_sub();
150 
151  // call the base destructors in the reverse order
152  for(irept::subt::const_reverse_iterator
153  bit=bases.rbegin();
154  bit!=bases.rend();
155  bit++)
156  {
157  assert(bit->id()==ID_base);
158  assert(bit->find(ID_type).id()==ID_symbol);
159  const symbolt &psymb = lookup(bit->find(ID_type).get(ID_identifier));
160 
161  // TODO(tautschnig): object is not type checked before passing it to
162  // cpp_destructor even though cpp_destructor makes heavy use of the .type()
163  // member
164  dereference_exprt object(exprt("cpp-this"), nil_typet());
165  object.add_source_location() = source_location;
166 
167  exprt dtor_code =
168  cpp_destructor(source_location, psymb.type, object);
169 
170  if(dtor_code.is_not_nil())
171  block.move_to_operands(dtor_code);
172  }
173 
174  return block;
175 }
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:43
bool is_not_nil() const
Definition: irep.h:103
std::vector< irept > subt
Definition: irep.h:90
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
subt & get_sub()
Definition: irep.h:245
const irep_idt & id() const
Definition: irep.h:189
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
Operator to dereference a pointer.
Definition: std_expr.h:3284
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)
Base class for tree-like data structures with sharing.
Definition: irep.h:86
C++ Language Type Checking.
Operator to return the address of an object.
Definition: std_expr.h:3170
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
The NIL type.
Definition: std_types.h:44
void make_nil()
Definition: irep.h:243
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
cpp_namet & name()
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:130
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
#define forall_irep(it, irep)
Definition: irep.h:61