cprover
Loading...
Searching...
No Matches
cpp_typecheck_initializer.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>
17#include <util/pointer_expr.h>
19
20#include "cpp_convert_type.h"
21#include "cpp_typecheck_fargs.h"
22
25{
26 // this is needed for template arguments that are types
27
28 if(symbol.is_type)
29 {
30 if(symbol.value.is_nil())
31 return;
32
33 if(symbol.value.id()!=ID_type)
34 {
36 error() << "expected type as initializer for '" << symbol.base_name << "'"
37 << eom;
38 throw 0;
39 }
40
41 typecheck_type(symbol.value.type());
42
43 return;
44 }
45
46 // do we have an initializer?
47 if(symbol.value.is_nil())
48 {
49 // do we need one?
50 if(is_reference(symbol.type))
51 {
53 error() << "'" << symbol.base_name
54 << "' is declared as reference but is not initialized" << eom;
55 throw 0;
56 }
57
58 // done
59 return;
60 }
61
62 // we do have an initializer
63
64 if(is_reference(symbol.type))
65 {
66 typecheck_expr(symbol.value);
67
68 if(has_auto(symbol.type))
69 {
71 typecheck_type(symbol.type);
72 implicit_typecast(symbol.value, symbol.type);
73 }
74
75 reference_initializer(symbol.value, symbol.type);
76 }
77 else if(cpp_is_pod(symbol.type))
78 {
79 if(
80 symbol.type.id() == ID_pointer &&
81 to_pointer_type(symbol.type).base_type().id() == ID_code &&
82 symbol.value.id() == ID_address_of &&
83 to_address_of_expr(symbol.value).object().id() == ID_cpp_name)
84 {
85 // initialization of a function pointer with
86 // the address of a function: use pointer type information
87 // for the sake of overload resolution
88
90 fargs.in_use = true;
91
92 const code_typet &code_type =
93 to_code_type(to_pointer_type(symbol.type).base_type());
94
95 for(const auto &parameter : code_type.parameters())
96 {
98 new_object.set(ID_C_lvalue, true);
99
100 if(parameter.get_this())
101 {
102 fargs.has_object = true;
103 new_object.type() = to_pointer_type(parameter.type()).base_type();
104 }
105
106 fargs.operands.push_back(new_object);
107 }
108
111 static_cast<irept &>(to_address_of_expr(symbol.value).object())),
113 fargs);
114
116 to_pointer_type(symbol.type).base_type() == resolved_expr.type(),
117 "symbol type must match");
118
119 if(resolved_expr.id()==ID_symbol)
120 {
121 symbol.value=
123 }
124 else if(resolved_expr.id()==ID_member)
125 {
126 symbol.value =
128 lookup(resolved_expr.get(ID_component_name)).symbol_expr());
129
130 symbol.value.type().add(ID_to_member) =
131 to_member_expr(resolved_expr).compound().type();
132 }
133 else
135
136 if(symbol.type != symbol.value.type())
137 {
139 error() << "conversion from '" << to_string(symbol.value.type())
140 << "' to '" << to_string(symbol.type) << "' " << eom;
141 throw 0;
142 }
143
144 return;
145 }
146
147 typecheck_expr(symbol.value);
148
149 if(symbol.value.type().find(ID_to_member).is_not_nil())
150 symbol.type.add(ID_to_member) = symbol.value.type().find(ID_to_member);
151
152 if(symbol.value.id()==ID_initializer_list ||
153 symbol.value.id()==ID_string_constant)
154 {
155 do_initializer(symbol.value, symbol.type, true);
156
157 if(symbol.type.find(ID_size).is_nil())
158 symbol.type=symbol.value.type();
159 }
160 else if(has_auto(symbol.type))
161 {
163 typecheck_type(symbol.type);
164 implicit_typecast(symbol.value, symbol.type);
165 }
166 else
167 implicit_typecast(symbol.value, symbol.type);
168
169 #if 0
171 exprt tmp_value = symbol.value;
172 if(!simplify.simplify(tmp_value))
173 symbol.value.swap(tmp_value);
174 #endif
175 }
176 else
177 {
178 // we need a constructor
179
180 symbol_exprt expr_symbol(symbol.name, symbol.type);
182
184 ops.push_back(symbol.value);
185
186 auto constructor =
188
189 if(constructor.has_value())
190 symbol.value = constructor.value();
191 else
192 symbol.value = nil_exprt();
193 }
194}
195
197 const exprt &object,
198 const typet &type,
199 const source_locationt &source_location,
201{
202 const typet &final_type=follow(type);
203
204 if(final_type.id()==ID_struct)
205 {
206 const auto &struct_type = to_struct_type(final_type);
207
208 if(struct_type.is_incomplete())
209 {
210 error().source_location = source_location;
211 error() << "cannot zero-initialize incomplete struct" << eom;
212 throw 0;
213 }
214
215 for(const auto &component : struct_type.components())
216 {
217 if(component.type().id()==ID_code)
218 continue;
219
220 if(component.get_bool(ID_is_type))
221 continue;
222
223 if(component.get_bool(ID_is_static))
224 continue;
225
226 member_exprt member(object, component.get_name(), component.type());
227
228 // recursive call
229 zero_initializer(member, component.type(), source_location, ops);
230 }
231 }
232 else if(
233 final_type.id() == ID_array &&
234 !cpp_is_pod(to_array_type(final_type).element_type()))
235 {
237 const exprt &size_expr=array_type.size();
238
239 if(size_expr.id()==ID_infinity)
240 return; // don't initialize
241
242 const mp_integer size =
244 CHECK_RETURN(size>=0);
245
247 for(mp_integer i=0; i<size; ++i)
248 {
249 index_exprt index(
250 object, from_integer(i, c_index_type()), array_type.element_type());
251 zero_initializer(index, array_type.element_type(), source_location, ops);
252 }
253 }
254 else if(final_type.id()==ID_union)
255 {
256 const auto &union_type = to_union_type(final_type);
257
258 if(union_type.is_incomplete())
259 {
260 error().source_location = source_location;
261 error() << "cannot zero-initialize incomplete union" << eom;
262 throw 0;
263 }
264
265 // Select the largest component for zero-initialization
267
269
270 for(const auto &component : union_type.components())
271 {
272 DATA_INVARIANT(component.type().is_not_nil(), "missing component type");
273
274 if(component.type().id()==ID_code)
275 continue;
276
277 auto component_size_opt = size_of_expr(component.type(), *this);
278
279 const auto size_int =
281 if(size_int.has_value())
282 {
284 {
287 }
288 }
289 }
290
291 if(max_comp_size>0)
292 {
293 const cpp_namet cpp_name(comp.get_base_name(), source_location);
294
295 exprt member(ID_member);
296 member.copy_to_operands(object);
298 zero_initializer(member, comp.type(), source_location, ops);
299 }
300 }
301 else if(final_type.id()==ID_c_enum)
302 {
304 to_bitvector_type(to_c_enum_type(final_type).underlying_type())
305 .get_width());
306
307 exprt zero =
310
312 assign.lhs()=object;
313 assign.rhs()=zero;
314 assign.add_source_location()=source_location;
315
316 typecheck_expr(assign.lhs());
317 assign.lhs().type().set(ID_C_constant, false);
319
320 typecheck_code(assign);
321 ops.push_back(assign);
322 }
323 else
324 {
325 const auto value = ::zero_initializer(final_type, source_location, *this);
326 if(!value.has_value())
327 {
328 error().source_location = source_location;
329 error() << "cannot zero-initialize '" << to_string(final_type) << "'"
330 << eom;
331 throw 0;
332 }
333
334 code_frontend_assignt assign(object, *value);
335 assign.add_source_location()=source_location;
336
337 typecheck_expr(assign.lhs());
338 assign.lhs().type().set(ID_C_constant, false);
340
341 typecheck_code(assign);
342 ops.push_back(assign);
343 }
344}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
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:563
static void make_already_typechecked(exprt &expr)
Arrays with given size.
Definition std_types.h:763
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A codet representing an assignment in the program.
Definition std_code.h:24
Base type of functions.
Definition std_types.h:539
void typecheck_type(typet &) override
void typecheck_code(codet &) override
void implicit_typecast(exprt &expr, const typet &type) override
bool cpp_is_pod(const typet &type) const
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
static bool has_auto(const typet &type)
void typecheck_expr(exprt &) override
std::string to_string(const typet &) override
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
void reference_initializer(exprt &expr, const typet &type)
A reference to type "cv1 T1" is initialized by an expression of type "cv2 T2" as follows:
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
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
Array index operator.
Definition std_expr.h:1410
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:372
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
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
bool is_nil() const
Definition irep.h:376
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
message_handlert & get_message_handler()
Definition message.h:184
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3026
Expression to hold a symbol (variable)
Definition std_expr.h:113
Symbol table entry.
Definition symbol.h:28
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
exprt value
Initial value of symbol.
Definition symbol.h:34
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
void cpp_convert_auto(typet &dest, const typet &src, message_handlert &message_handler)
C++ Language Conversion.
cpp_namet & to_cpp_name(irept &cpp_name)
Definition cpp_name.h:148
C++ Language Type Checking.
C++ Language Type Checking.
Expression Initialization.
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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
#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
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:77
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:2886
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