CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
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 if(type.id() == ID_struct_tag)
203 {
204 const auto &struct_type = follow_tag(to_struct_tag_type(type));
205
206 if(struct_type.is_incomplete())
207 {
208 error().source_location = source_location;
209 error() << "cannot zero-initialize incomplete struct" << eom;
210 throw 0;
211 }
212
213 for(const auto &component : struct_type.components())
214 {
215 if(component.type().id()==ID_code)
216 continue;
217
218 if(component.get_bool(ID_is_type))
219 continue;
220
221 if(component.get_bool(ID_is_static))
222 continue;
223
224 member_exprt member(object, component.get_name(), component.type());
225
226 // recursive call
227 zero_initializer(member, component.type(), source_location, ops);
228 }
229 }
230 else if(
231 type.id() == ID_array && !cpp_is_pod(to_array_type(type).element_type()))
232 {
234 const exprt &size_expr=array_type.size();
235
236 if(size_expr.id()==ID_infinity)
237 return; // don't initialize
238
239 const mp_integer size =
241 CHECK_RETURN(size>=0);
242
244 for(mp_integer i=0; i<size; ++i)
245 {
246 index_exprt index(
247 object, from_integer(i, c_index_type()), array_type.element_type());
248 zero_initializer(index, array_type.element_type(), source_location, ops);
249 }
250 }
251 else if(type.id() == ID_union_tag)
252 {
253 const auto &union_type = follow_tag(to_union_tag_type(type));
254
255 if(union_type.is_incomplete())
256 {
257 error().source_location = source_location;
258 error() << "cannot zero-initialize incomplete union" << eom;
259 throw 0;
260 }
261
262 // Select the largest component for zero-initialization
264
266
267 for(const auto &component : union_type.components())
268 {
269 DATA_INVARIANT(component.type().is_not_nil(), "missing component type");
270
271 if(component.type().id()==ID_code)
272 continue;
273
274 auto component_size_opt = size_of_expr(component.type(), *this);
275
276 const auto size_int =
278 if(size_int.has_value())
279 {
281 {
284 }
285 }
286 }
287
288 if(max_comp_size>0)
289 {
290 const cpp_namet cpp_name(comp.get_base_name(), source_location);
291
292 exprt member(ID_member);
293 member.copy_to_operands(object);
295 zero_initializer(member, comp.type(), source_location, ops);
296 }
297 }
298 else if(type.id() == ID_c_enum_tag)
299 {
301 to_bitvector_type(follow_tag(to_c_enum_tag_type(type)).underlying_type())
302 .get_width());
303
304 exprt zero =
307
309 assign.lhs()=object;
310 assign.rhs()=zero;
311 assign.add_source_location()=source_location;
312
313 typecheck_expr(assign.lhs());
314 assign.lhs().type().set(ID_C_constant, false);
316
317 typecheck_code(assign);
318 ops.push_back(assign);
319 }
320 else
321 {
322 const auto value = ::zero_initializer(type, source_location, *this);
323 if(!value.has_value())
324 {
325 error().source_location = source_location;
326 error() << "cannot zero-initialize '" << to_string(type) << "'" << eom;
327 throw 0;
328 }
329
330 code_frontend_assignt assign(object, *value);
331 assign.add_source_location()=source_location;
332
333 typecheck_expr(assign.lhs());
334 assign.lhs().type().set(ID_C_constant, false);
336
337 typecheck_code(assign);
338 ops.push_back(assign);
339 }
340}
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_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
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)
Arrays with given size.
Definition std_types.h:807
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:583
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.
std::optional< 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 reference_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:163
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
Array index operator.
Definition std_expr.h:1470
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
const irept & find(const irep_idt &name) const
Definition irep.cpp:93
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
bool is_nil() const
Definition irep.h:368
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
message_handlert & get_message_handler()
Definition message.h:183
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3208
Expression to hold a symbol (variable)
Definition std_expr.h:131
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:2081
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 reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
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.
std::optional< 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:97
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
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