CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_constructor.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
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/pointer_expr.h>
17
23 const source_locationt &source_location,
24 const exprt &object,
25 const exprt::operandst &operands)
26{
27 exprt object_tc=object;
28
30
32
34
35 if(object_tc.type().id() == ID_array)
36 {
37 // We allow only one operand and it must be tagged with '#array_ini'.
38 // Note that the operand is an array that is used for copy-initialization.
39 // In the general case, a program is not allowed to use this form of
40 // construct. This way of initializing an array is used internally only.
41 // The purpose of the tag #array_ini is to rule out ill-formed
42 // programs.
43
44 if(!operands.empty() && !operands.front().get_bool(ID_C_array_ini))
45 {
46 error().source_location=source_location;
47 error() << "bad array initializer" << eom;
48 throw 0;
49 }
50
52 operands.empty() || operands.size() == 1,
53 "array constructor must have at most one operand");
54
55 if(operands.empty() && cpp_is_pod(object_tc.type()))
56 return {};
57
58 const exprt &size_expr = to_array_type(object_tc.type()).size();
59
60 if(size_expr.id() == ID_infinity)
61 return {}; // don't initialize
62
65
66 mp_integer s;
68 {
69 error().source_location=source_location;
70 error() << "array size '" << to_string(size_expr) << "' is not a constant"
71 << eom;
72 throw 0;
73 }
74
75 /*if(cpp_is_pod(object_tc.type()))
76 {
77 code_expressiont new_code;
78 exprt op_tc=operands.front();
79 typecheck_expr(op_tc);
80 // Override constantness
81 object_tc.type().set("ID_C_constant", false);
82 object_tc.set("ID_C_lvalue", true);
83 side_effect_exprt assign(ID_assign);
84 assign.add_source_location()=source_location;
85 assign.copy_to_operands(object_tc, op_tc);
86 typecheck_side_effect_assignment(assign);
87 new_code.expression()=assign;
88 return new_code;
89 }
90 else*/
91 {
92 code_blockt new_code;
93
94 // for each element of the array, call the default constructor
95 for(mp_integer i=0; i < s; ++i)
96 {
98
99 exprt constant = from_integer(i, c_index_type());
100 constant.add_source_location()=source_location;
101
102 index_exprt index = index_exprt(object_tc, constant);
103 index.add_source_location()=source_location;
104
105 if(!operands.empty())
106 {
107 index_exprt operand(operands.front(), constant);
108 operand.add_source_location()=source_location;
109 tmp_operands.push_back(operand);
110 }
111
112 auto i_code = cpp_constructor(source_location, index, tmp_operands);
113
114 if(i_code.has_value())
115 new_code.add(std::move(i_code.value()));
116 }
117 return std::move(new_code);
118 }
119 }
120 else if(cpp_is_pod(object_tc.type()))
121 {
123
124 for(auto &op : operands_tc)
125 {
126 typecheck_expr(op);
128 }
129
130 if(operands_tc.empty())
131 {
132 // a POD is NOT initialized
133 return {};
134 }
135 else if(operands_tc.size()==1)
136 {
137 // Override constantness
138 object_tc.type().set(ID_C_constant, false);
139 object_tc.set(ID_C_lvalue, true);
141 object_tc, operands_tc.front(), typet(), source_location);
143 return code_expressiont(std::move(assign));
144 }
145 else
146 {
147 error().source_location=source_location;
148 error() << "initialization of POD requires one argument, "
149 "but got " << operands.size() << eom;
150 throw 0;
151 }
152 }
153 else if(object_tc.type().id() == ID_union_tag)
154 {
155 UNREACHABLE; // Todo: union
156 }
157 else if(object_tc.type().id() == ID_struct_tag)
158 {
160
161 for(auto &op : operands_tc)
162 {
163 typecheck_expr(op);
165 }
166
169
170 // set most-derived bits
171 code_blockt block;
172 for(const auto &component : struct_type.components())
173 {
174 if(component.get_base_name() != "@most_derived")
175 continue;
176
177 member_exprt member(object_tc, component.get_name(), bool_typet());
178 member.add_source_location()=source_location;
179 member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue));
180
182
183 if(!component.get_bool(ID_from_base))
184 val=true_exprt();
185
187 std::move(member), std::move(val), typet(), source_location);
188
190
191 block.add(code_expressiont(std::move(assign)));
192 }
193
194 // enter struct scope
197
198 // find name of constructor
199 const struct_typet::componentst &components=
200 struct_type.components();
201
203
204 for(const auto &c : components)
205 {
206 const typet &type = c.type();
207
208 if(
209 !c.get_bool(ID_from_base) && type.id() == ID_code &&
210 to_code_type(type).return_type().id() == ID_constructor)
211 {
212 constructor_name = c.get_base_name();
213 break;
214 }
215 }
216
217 INVARIANT(!constructor_name.empty(), "non-PODs should have a constructor");
218
220 cpp_namet(constructor_name, source_location).as_expr(),
223 source_location);
224
227
228 exprt &initializer =
229 static_cast<exprt &>(function_call.add(ID_initializer));
230
232 initializer.id() == ID_code &&
233 initializer.get(ID_statement) == ID_expression,
234 "initializer must be expression statement");
235
236 auto &statement_expr = to_code_expression(to_code(initializer));
237
240
241 exprt &tmp_this=func_ini.arguments().front();
243 to_address_of_expr(tmp_this).object().id() == ID_new_object,
244 "expected new_object operand in address_of expression");
245
247
248 const auto &initializer_code=to_code(initializer);
249
250 if(block.statements().empty())
251 return initializer_code;
252 else
253 {
254 block.add(initializer_code);
255 return std::move(block);
256 }
257 }
258 else
260
261 return {};
262}
263
265 const source_locationt &source_location,
266 const typet &type,
267 const exprt::operandst &ops,
269{
270 // create temporary object
273
275 new_object.add_source_location()=tmp_object_expr.source_location();
276 new_object.set(ID_C_lvalue, true);
277 new_object.type()=tmp_object_expr.type();
278
280
281 auto new_code = cpp_constructor(source_location, new_object, ops);
282
283 if(new_code.has_value())
284 {
285 if(new_code->get_statement() == ID_assign)
286 tmp_object_expr.add_to_operands(std::move(new_code->op1()));
287 else
288 tmp_object_expr.add(ID_initializer) = *new_code;
289 }
290
292}
293
295 const source_locationt &source_location,
296 const typet &type,
297 const exprt &op,
299{
301 ops.push_back(op);
302 new_temporary(source_location, type, ops, temporary);
303}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
static void make_already_typechecked(exprt &expr)
The Boolean type.
Definition std_types.h:36
virtual void make_constant_index(exprt &expr)
A codet representing sequential composition of program statements.
Definition std_code.h:130
code_operandst & statements()
Definition std_code.h:138
void add(const codet &code)
Definition std_code.h:168
codet representation of an expression statement.
Definition std_code.h:1394
cpp_scopet & set_scope(const irep_idt &identifier)
Definition cpp_scopes.h:87
void typecheck_side_effect_assignment(side_effect_exprt &) override
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void elaborate_class_template(const typet &type)
elaborate class template instances
void add_implicit_dereference(exprt &)
void typecheck_expr(exprt &) override
std::string to_string(const typet &) override
cpp_scopest cpp_scopes
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
source_locationt & add_source_location()
Definition expr.h:236
The Boolean constant false.
Definition std_expr.h:3199
Array index operator.
Definition std_expr.h:1470
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
Extract member of struct or union.
Definition std_expr.h:2971
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A side_effect_exprt that performs an assignment.
Definition std_code.h:1565
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
An expression containing a side effect.
Definition std_code.h:1450
Structure type, corresponds to C style structs.
Definition std_types.h:231
std::vector< componentt > componentst
Definition std_types.h:140
The Boolean constant true.
Definition std_expr.h:3190
The type of an expression, extends irept.
Definition type.h:29
C++ Language Type Checking.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
code_expressiont & to_code_expression(codet &code)
Definition std_code.h:1428
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:97
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888