cprover
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 
24 {
25  // this is needed for template arguments that are types
26 
27  if(symbol.is_type)
28  {
29  if(symbol.value.is_nil())
30  return;
31 
32  if(symbol.value.id()!=ID_type)
33  {
35  error() << "expected type as initializer for '" << symbol.base_name << "'"
36  << eom;
37  throw 0;
38  }
39 
40  typecheck_type(symbol.value.type());
41 
42  return;
43  }
44 
45  // do we have an initializer?
46  if(symbol.value.is_nil())
47  {
48  // do we need one?
49  if(is_reference(symbol.type))
50  {
52  error() << "'" << symbol.base_name
53  << "' is declared as reference but is not initialized" << eom;
54  throw 0;
55  }
56 
57  // done
58  return;
59  }
60 
61  // we do have an initializer
62 
63  if(is_reference(symbol.type))
64  {
65  typecheck_expr(symbol.value);
66 
67  if(has_auto(symbol.type))
68  {
69  cpp_convert_auto(symbol.type, symbol.value.type(), get_message_handler());
70  typecheck_type(symbol.type);
71  implicit_typecast(symbol.value, symbol.type);
72  }
73 
74  reference_initializer(symbol.value, symbol.type);
75  }
76  else if(cpp_is_pod(symbol.type))
77  {
78  if(
79  symbol.type.id() == ID_pointer && symbol.type.subtype().id() == ID_code &&
80  symbol.value.id() == ID_address_of &&
81  to_address_of_expr(symbol.value).object().id() == ID_cpp_name)
82  {
83  // initialization of a function pointer with
84  // the address of a function: use pointer type information
85  // for the sake of overload resolution
86 
88  fargs.in_use = true;
89 
90  const code_typet &code_type=to_code_type(symbol.type.subtype());
91 
92  for(const auto &parameter : code_type.parameters())
93  {
94  exprt new_object(ID_new_object, parameter.type());
95  new_object.set(ID_C_lvalue, true);
96 
97  if(parameter.get_this())
98  {
99  fargs.has_object = true;
100  new_object.type() = parameter.type().subtype();
101  }
102 
103  fargs.operands.push_back(new_object);
104  }
105 
106  exprt resolved_expr = resolve(
107  to_cpp_name(
108  static_cast<irept &>(to_address_of_expr(symbol.value).object())),
110  fargs);
111 
112  assert(symbol.type.subtype() == resolved_expr.type());
113 
114  if(resolved_expr.id()==ID_symbol)
115  {
116  symbol.value=
117  address_of_exprt(resolved_expr);
118  }
119  else if(resolved_expr.id()==ID_member)
120  {
121  symbol.value =
123  lookup(resolved_expr.get(ID_component_name)).symbol_expr());
124 
125  symbol.value.type().add(ID_to_member) =
126  to_member_expr(resolved_expr).compound().type();
127  }
128  else
129  UNREACHABLE;
130 
131  if(symbol.type != symbol.value.type())
132  {
133  error().source_location=symbol.location;
134  error() << "conversion from '" << to_string(symbol.value.type())
135  << "' to '" << to_string(symbol.type) << "' " << eom;
136  throw 0;
137  }
138 
139  return;
140  }
141 
142  typecheck_expr(symbol.value);
143 
144  if(symbol.value.type().find(ID_to_member).is_not_nil())
145  symbol.type.add(ID_to_member) = symbol.value.type().find(ID_to_member);
146 
147  if(symbol.value.id()==ID_initializer_list ||
148  symbol.value.id()==ID_string_constant)
149  {
150  do_initializer(symbol.value, symbol.type, true);
151 
152  if(symbol.type.find(ID_size).is_nil())
153  symbol.type=symbol.value.type();
154  }
155  else if(has_auto(symbol.type))
156  {
157  cpp_convert_auto(symbol.type, symbol.value.type(), get_message_handler());
158  typecheck_type(symbol.type);
159  implicit_typecast(symbol.value, symbol.type);
160  }
161  else
162  implicit_typecast(symbol.value, symbol.type);
163 
164  #if 0
165  simplify_exprt simplify(*this);
166  exprt tmp_value = symbol.value;
167  if(!simplify.simplify(tmp_value))
168  symbol.value.swap(tmp_value);
169  #endif
170  }
171  else
172  {
173  // we need a constructor
174 
175  symbol_exprt expr_symbol(symbol.name, symbol.type);
177 
178  exprt::operandst ops;
179  ops.push_back(symbol.value);
180 
181  auto constructor =
182  cpp_constructor(symbol.value.source_location(), expr_symbol, ops);
183 
184  if(constructor.has_value())
185  symbol.value = constructor.value();
186  else
187  symbol.value = nil_exprt();
188  }
189 }
190 
192  const exprt &object,
193  const typet &type,
194  const source_locationt &source_location,
195  exprt::operandst &ops)
196 {
197  const typet &final_type=follow(type);
198 
199  if(final_type.id()==ID_struct)
200  {
201  const auto &struct_type = to_struct_type(final_type);
202 
203  if(struct_type.is_incomplete())
204  {
205  error().source_location = source_location;
206  error() << "cannot zero-initialize incomplete struct" << eom;
207  throw 0;
208  }
209 
210  for(const auto &component : struct_type.components())
211  {
212  if(component.type().id()==ID_code)
213  continue;
214 
215  if(component.get_bool(ID_is_type))
216  continue;
217 
218  if(component.get_bool(ID_is_static))
219  continue;
220 
221  member_exprt member(object, component.get_name(), component.type());
222 
223  // recursive call
224  zero_initializer(member, component.type(), source_location, ops);
225  }
226  }
227  else if(final_type.id()==ID_array &&
228  !cpp_is_pod(final_type.subtype()))
229  {
230  const array_typet &array_type=to_array_type(type);
231  const exprt &size_expr=array_type.size();
232 
233  if(size_expr.id()==ID_infinity)
234  return; // don't initialize
235 
236  const mp_integer size =
237  numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
238  CHECK_RETURN(size>=0);
239 
240  exprt::operandst empty_operands;
241  for(mp_integer i=0; i<size; ++i)
242  {
243  index_exprt index(
244  object, from_integer(i, index_type()), array_type.subtype());
245  zero_initializer(index, array_type.subtype(), source_location, ops);
246  }
247  }
248  else if(final_type.id()==ID_union)
249  {
250  const auto &union_type = to_union_type(final_type);
251 
252  if(union_type.is_incomplete())
253  {
254  error().source_location = source_location;
255  error() << "cannot zero-initialize incomplete union" << eom;
256  throw 0;
257  }
258 
259  // Select the largest component for zero-initialization
260  mp_integer max_comp_size=0;
261 
263 
264  for(const auto &component : union_type.components())
265  {
266  assert(component.type().is_not_nil());
267 
268  if(component.type().id()==ID_code)
269  continue;
270 
271  auto component_size_opt = size_of_expr(component.type(), *this);
272 
273  const auto size_int =
274  numeric_cast<mp_integer>(component_size_opt.value_or(nil_exprt()));
275  if(size_int.has_value())
276  {
277  if(*size_int > max_comp_size)
278  {
279  max_comp_size = *size_int;
280  comp=component;
281  }
282  }
283  }
284 
285  if(max_comp_size>0)
286  {
287  const cpp_namet cpp_name(comp.get_base_name(), source_location);
288 
289  exprt member(ID_member);
290  member.copy_to_operands(object);
291  member.set(ID_component_cpp_name, cpp_name);
292  zero_initializer(member, comp.type(), source_location, ops);
293  }
294  }
295  else if(final_type.id()==ID_c_enum)
296  {
297  const unsignedbv_typet enum_type(
298  to_bitvector_type(final_type.subtype()).get_width());
299 
300  exprt zero =
301  typecast_exprt::conditional_cast(from_integer(0, enum_type), type);
303 
304  code_assignt assign;
305  assign.lhs()=object;
306  assign.rhs()=zero;
307  assign.add_source_location()=source_location;
308 
309  typecheck_expr(assign.lhs());
310  assign.lhs().type().set(ID_C_constant, false);
312 
313  typecheck_code(assign);
314  ops.push_back(assign);
315  }
316  else
317  {
318  const auto value = ::zero_initializer(final_type, source_location, *this);
319  if(!value.has_value())
320  {
321  error().source_location = source_location;
322  error() << "cannot zero-initialize '" << to_string(final_type) << "'"
323  << eom;
324  throw 0;
325  }
326 
327  code_assignt assign(object, *value);
328  assign.add_source_location()=source_location;
329 
330  typecheck_expr(assign.lhs());
331  assign.lhs().type().set(ID_C_constant, false);
333 
334  typecheck_code(assign);
335  ops.push_back(assign);
336  }
337 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: pointer_expr.h:200
exprt & object()
Definition: pointer_expr.h:209
static void make_already_typechecked(exprt &expr)
Arrays with given size.
Definition: std_types.h:968
const exprt & size() const
Definition: std_types.h:976
std::size_t get_width() const
Definition: std_types.h:1048
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt & rhs()
Definition: std_code.h:317
exprt & lhs()
Definition: std_code.h:312
Base type of functions.
Definition: std_types.h:744
const parameterst & parameters() const
Definition: std_types.h:860
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:14
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)
Definition: cpp_typecheck.h:88
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:54
std::vector< exprt > operandst
Definition: expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:133
source_locationt & add_source_location()
Definition: expr.h:239
const source_locationt & source_location() const
Definition: expr.h:234
typet & type()
Return the type of the expression.
Definition: expr.h:82
Array index operator.
Definition: std_expr.h:1243
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
irept & add(const irep_namet &name)
Definition: irep.cpp:113
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_nil() const
Definition: irep.h:387
Extract member of struct or union.
Definition: std_expr.h:2528
const exprt & compound() const
Definition: std_expr.h:2569
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:51
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
The NIL expression.
Definition: std_expr.h:2735
const irep_idt & get_base_name() const
Definition: std_types.h:84
Expression to hold a symbol (variable)
Definition: std_expr.h:81
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:122
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:1789
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
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.
Expression Initialization.
BigInt mp_integer
Definition: mp_arith.h:19
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
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:496
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:55
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:147
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:430