CBMC
cpp_typecheck_initializer.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 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/expr_initializer.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  {
70  cpp_convert_auto(symbol.type, symbol.value.type(), get_message_handler());
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 =
94 
95  for(const auto &parameter : code_type.parameters())
96  {
97  exprt new_object(ID_new_object, parameter.type());
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 
109  exprt resolved_expr = resolve(
110  to_cpp_name(
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=
122  address_of_exprt(resolved_expr);
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
134  UNREACHABLE;
135 
136  if(symbol.type != symbol.value.type())
137  {
138  error().source_location=symbol.location;
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  {
162  cpp_convert_auto(symbol.type, symbol.value.type(), get_message_handler());
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
170  simplify_exprt simplify(*this);
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 
183  exprt::operandst ops;
184  ops.push_back(symbol.value);
185 
186  auto constructor =
187  cpp_constructor(symbol.value.source_location(), expr_symbol, ops);
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,
200  exprt::operandst &ops)
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  {
233  const array_typet &array_type=to_array_type(type);
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 =
240  numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
241  CHECK_RETURN(size>=0);
242 
243  exprt::operandst empty_operands;
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
263  mp_integer max_comp_size=0;
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 =
277  numeric_cast<mp_integer>(component_size_opt.value_or(nil_exprt()));
278  if(size_int.has_value())
279  {
280  if(*size_int > max_comp_size)
281  {
282  max_comp_size = *size_int;
283  comp=component;
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);
294  member.set(ID_component_cpp_name, cpp_name);
295  zero_initializer(member, comp.type(), source_location, ops);
296  }
297  }
298  else if(type.id() == ID_c_enum_tag)
299  {
300  const unsignedbv_typet enum_type(
301  to_bitvector_type(follow_tag(to_c_enum_tag_type(type)).underlying_type())
302  .get_width());
303 
304  exprt zero =
305  typecast_exprt::conditional_cast(from_integer(0, enum_type), type);
307 
308  code_frontend_assignt assign;
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 union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
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
Operator to return the address of an object.
Definition: pointer_expr.h:540
exprt & object()
Definition: pointer_expr.h:549
static void make_already_typechecked(exprt &expr)
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
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
const parameterst & parameters() const
Definition: std_types.h:699
exprt::operandst operands
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
Definition: cpp_is_pod.cpp:16
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)
Definition: cpp_typecheck.h:71
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
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
Array index operator.
Definition: std_expr.h:1465
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
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
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
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:2844
const exprt & compound() const
Definition: std_expr.h:2893
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:63
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
The NIL expression.
Definition: std_expr.h:3081
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
const irep_idt & get_base_name() const
Definition: std_types.h:89
Expression to hold a symbol (variable)
Definition: std_expr.h:131
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
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.
Definition: std_types.cpp:145
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const reference_typet & to_reference_type(const typet &type)
Cast a typet to a reference_typet.
Definition: pointer_expr.h:162
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
bool simplify(exprt &expr, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#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 constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518