cprover
Loading...
Searching...
No Matches
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
29 typecheck_expr(object_tc);
30
31 elaborate_class_template(object_tc.type());
32
33 typet tmp_type(follow(object_tc.type()));
34 CHECK_RETURN(!is_reference(tmp_type));
35
36 if(tmp_type.id()==ID_array)
37 {
38 // We allow only one operand and it must be tagged with '#array_ini'.
39 // Note that the operand is an array that is used for copy-initialization.
40 // In the general case, a program is not allowed to use this form of
41 // construct. This way of initializing an array is used internally only.
42 // The purpose of the tag #array_ini is to rule out ill-formed
43 // programs.
44
45 if(!operands.empty() && !operands.front().get_bool(ID_C_array_ini))
46 {
47 error().source_location=source_location;
48 error() << "bad array initializer" << eom;
49 throw 0;
50 }
51
53 operands.empty() || operands.size() == 1,
54 "array constructor must have at most one operand");
55
56 if(operands.empty() && cpp_is_pod(tmp_type))
57 return {};
58
59 const exprt &size_expr=
60 to_array_type(tmp_type).size();
61
62 if(size_expr.id() == ID_infinity)
63 return {}; // don't initialize
64
65 exprt tmp_size=size_expr;
66 make_constant_index(tmp_size);
67
68 mp_integer s;
69 if(to_integer(to_constant_expr(tmp_size), s))
70 {
71 error().source_location=source_location;
72 error() << "array size '" << to_string(size_expr) << "' is not a constant"
73 << eom;
74 throw 0;
75 }
76
77 /*if(cpp_is_pod(tmp_type))
78 {
79 code_expressiont new_code;
80 exprt op_tc=operands.front();
81 typecheck_expr(op_tc);
82 // Override constantness
83 object_tc.type().set("ID_C_constant", false);
84 object_tc.set("ID_C_lvalue", true);
85 side_effect_exprt assign(ID_assign);
86 assign.add_source_location()=source_location;
87 assign.copy_to_operands(object_tc, op_tc);
88 typecheck_side_effect_assignment(assign);
89 new_code.expression()=assign;
90 return new_code;
91 }
92 else*/
93 {
94 code_blockt new_code;
95
96 // for each element of the array, call the default constructor
97 for(mp_integer i=0; i < s; ++i)
98 {
99 exprt::operandst tmp_operands;
100
101 exprt constant = from_integer(i, c_index_type());
102 constant.add_source_location()=source_location;
103
104 index_exprt index = index_exprt(object_tc, constant);
105 index.add_source_location()=source_location;
106
107 if(!operands.empty())
108 {
109 index_exprt operand(operands.front(), constant);
110 operand.add_source_location()=source_location;
111 tmp_operands.push_back(operand);
112 }
113
114 auto i_code = cpp_constructor(source_location, index, tmp_operands);
115
116 if(i_code.has_value())
117 new_code.add(std::move(i_code.value()));
118 }
119 return std::move(new_code);
120 }
121 }
122 else if(cpp_is_pod(tmp_type))
123 {
124 exprt::operandst operands_tc=operands;
125
126 for(auto &op : operands_tc)
127 {
128 typecheck_expr(op);
130 }
131
132 if(operands_tc.empty())
133 {
134 // a POD is NOT initialized
135 return {};
136 }
137 else if(operands_tc.size()==1)
138 {
139 // Override constantness
140 object_tc.type().set(ID_C_constant, false);
141 object_tc.set(ID_C_lvalue, true);
143 object_tc, operands_tc.front(), typet(), source_location);
145 return code_expressiont(std::move(assign));
146 }
147 else
148 {
149 error().source_location=source_location;
150 error() << "initialization of POD requires one argument, "
151 "but got " << operands.size() << eom;
152 throw 0;
153 }
154 }
155 else if(tmp_type.id()==ID_union)
156 {
157 UNREACHABLE; // Todo: union
158 }
159 else if(tmp_type.id()==ID_struct)
160 {
161 exprt::operandst operands_tc=operands;
162
163 for(auto &op : operands_tc)
164 {
165 typecheck_expr(op);
167 }
168
169 const struct_typet &struct_type=
170 to_struct_type(tmp_type);
171
172 // set most-derived bits
173 code_blockt block;
174 for(const auto &component : struct_type.components())
175 {
176 if(component.get_base_name() != "@most_derived")
177 continue;
178
179 member_exprt member(object_tc, component.get_name(), bool_typet());
180 member.add_source_location()=source_location;
181 member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue));
182
183 exprt val=false_exprt();
184
185 if(!component.get_bool(ID_from_base))
186 val=true_exprt();
187
189 std::move(member), std::move(val), typet(), source_location);
190
192
193 block.add(code_expressiont(std::move(assign)));
194 }
195
196 // enter struct scope
197 cpp_save_scopet save_scope(cpp_scopes);
198 cpp_scopes.set_scope(struct_type.get(ID_name));
199
200 // find name of constructor
201 const struct_typet::componentst &components=
202 struct_type.components();
203
204 irep_idt constructor_name;
205
206 for(const auto &c : components)
207 {
208 const typet &type = c.type();
209
210 if(
211 !c.get_bool(ID_from_base) && type.id() == ID_code &&
212 to_code_type(type).return_type().id() == ID_constructor)
213 {
214 constructor_name = c.get_base_name();
215 break;
216 }
217 }
218
219 INVARIANT(!constructor_name.empty(), "non-PODs should have a constructor");
220
222 cpp_namet(constructor_name, source_location).as_expr(),
223 operands_tc,
225 source_location);
226
228 CHECK_RETURN(function_call.get(ID_statement) == ID_temporary_object);
229
230 exprt &initializer =
231 static_cast<exprt &>(function_call.add(ID_initializer));
232
234 initializer.id() == ID_code &&
235 initializer.get(ID_statement) == ID_expression,
236 "initializer must be expression statement");
237
238 auto &statement_expr = to_code_expression(to_code(initializer));
239
241 to_side_effect_expr_function_call(statement_expr.expression());
242
243 exprt &tmp_this=func_ini.arguments().front();
245 to_address_of_expr(tmp_this).object().id() == ID_new_object,
246 "expected new_object operand in address_of expression");
247
248 tmp_this=address_of_exprt(object_tc);
249
250 const auto &initializer_code=to_code(initializer);
251
252 if(block.statements().empty())
253 return initializer_code;
254 else
255 {
256 block.add(initializer_code);
257 return std::move(block);
258 }
259 }
260 else
262
263 return {};
264}
265
267 const source_locationt &source_location,
268 const typet &type,
269 const exprt::operandst &ops,
270 exprt &temporary)
271{
272 // create temporary object
273 side_effect_exprt tmp_object_expr(ID_temporary_object, type, source_location);
274 tmp_object_expr.set(ID_mode, ID_cpp);
275
276 exprt new_object(ID_new_object);
277 new_object.add_source_location()=tmp_object_expr.source_location();
278 new_object.set(ID_C_lvalue, true);
279 new_object.type()=tmp_object_expr.type();
280
282
283 auto new_code = cpp_constructor(source_location, new_object, ops);
284
285 if(new_code.has_value())
286 {
287 if(new_code->get_statement() == ID_assign)
288 tmp_object_expr.add_to_operands(std::move(new_code->op1()));
289 else
290 tmp_object_expr.add(ID_initializer) = *new_code;
291 }
292
293 temporary.swap(tmp_object_expr);
294}
295
297 const source_locationt &source_location,
298 const typet &type,
299 const exprt &op,
300 exprt &temporary)
301{
303 ops.push_back(op);
304 new_temporary(source_location, type, ops, temporary);
305}
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.
static void make_already_typechecked(exprt &expr)
const exprt & size() const
Definition std_types.h:796
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
const typet & return_type() const
Definition std_types.h:645
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)
optionalt< 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:39
bool empty() const
Definition dstring.h:90
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:223
source_locationt & add_source_location()
Definition expr.h:228
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
The Boolean constant false.
Definition std_expr.h:3017
Array index operator.
Definition std_expr.h:1410
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
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:420
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
Extract member of struct or union.
Definition std_expr.h:2794
source_locationt source_location
Definition message.h:247
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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
exprt::operandst & arguments()
Definition std_code.h:1718
An expression containing a side effect.
Definition std_code.h:1450
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The Boolean constant true.
Definition std_expr.h:3008
The type of an expression, extends irept.
Definition type.h:29
C++ Language Type Checking.
nonstd::optional< T > optionalt
Definition optional.h:35
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.
BigInt mp_integer
Definition smt_terms.h:18
#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:77
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844