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 #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 
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 && symbol.type.subtype().id() == ID_code &&
81  symbol.value.id() == ID_address_of &&
82  to_address_of_expr(symbol.value).object().id() == ID_cpp_name)
83  {
84  // initialization of a function pointer with
85  // the address of a function: use pointer type information
86  // for the sake of overload resolution
87 
89  fargs.in_use = true;
90 
91  const code_typet &code_type=to_code_type(symbol.type.subtype());
92 
93  for(const auto &parameter : code_type.parameters())
94  {
95  exprt new_object(ID_new_object, parameter.type());
96  new_object.set(ID_C_lvalue, true);
97 
98  if(parameter.get_this())
99  {
100  fargs.has_object = true;
101  new_object.type() = parameter.type().subtype();
102  }
103 
104  fargs.operands.push_back(new_object);
105  }
106 
107  exprt resolved_expr = resolve(
108  to_cpp_name(
109  static_cast<irept &>(to_address_of_expr(symbol.value).object())),
111  fargs);
112 
113  assert(symbol.type.subtype() == resolved_expr.type());
114 
115  if(resolved_expr.id()==ID_symbol)
116  {
117  symbol.value=
118  address_of_exprt(resolved_expr);
119  }
120  else if(resolved_expr.id()==ID_member)
121  {
122  symbol.value =
124  lookup(resolved_expr.get(ID_component_name)).symbol_expr());
125 
126  symbol.value.type().add(ID_to_member) =
127  to_member_expr(resolved_expr).compound().type();
128  }
129  else
130  UNREACHABLE;
131 
132  if(symbol.type != symbol.value.type())
133  {
134  error().source_location=symbol.location;
135  error() << "conversion from '" << to_string(symbol.value.type())
136  << "' to '" << to_string(symbol.type) << "' " << eom;
137  throw 0;
138  }
139 
140  return;
141  }
142 
143  typecheck_expr(symbol.value);
144 
145  if(symbol.value.type().find(ID_to_member).is_not_nil())
146  symbol.type.add(ID_to_member) = symbol.value.type().find(ID_to_member);
147 
148  if(symbol.value.id()==ID_initializer_list ||
149  symbol.value.id()==ID_string_constant)
150  {
151  do_initializer(symbol.value, symbol.type, true);
152 
153  if(symbol.type.find(ID_size).is_nil())
154  symbol.type=symbol.value.type();
155  }
156  else if(has_auto(symbol.type))
157  {
158  cpp_convert_auto(symbol.type, symbol.value.type(), get_message_handler());
159  typecheck_type(symbol.type);
160  implicit_typecast(symbol.value, symbol.type);
161  }
162  else
163  implicit_typecast(symbol.value, symbol.type);
164 
165  #if 0
166  simplify_exprt simplify(*this);
167  exprt tmp_value = symbol.value;
168  if(!simplify.simplify(tmp_value))
169  symbol.value.swap(tmp_value);
170  #endif
171  }
172  else
173  {
174  // we need a constructor
175 
176  symbol_exprt expr_symbol(symbol.name, symbol.type);
178 
179  exprt::operandst ops;
180  ops.push_back(symbol.value);
181 
182  auto constructor =
183  cpp_constructor(symbol.value.source_location(), expr_symbol, ops);
184 
185  if(constructor.has_value())
186  symbol.value = constructor.value();
187  else
188  symbol.value = nil_exprt();
189  }
190 }
191 
193  const exprt &object,
194  const typet &type,
195  const source_locationt &source_location,
196  exprt::operandst &ops)
197 {
198  const typet &final_type=follow(type);
199 
200  if(final_type.id()==ID_struct)
201  {
202  const auto &struct_type = to_struct_type(final_type);
203 
204  if(struct_type.is_incomplete())
205  {
206  error().source_location = source_location;
207  error() << "cannot zero-initialize incomplete struct" << eom;
208  throw 0;
209  }
210 
211  for(const auto &component : struct_type.components())
212  {
213  if(component.type().id()==ID_code)
214  continue;
215 
216  if(component.get_bool(ID_is_type))
217  continue;
218 
219  if(component.get_bool(ID_is_static))
220  continue;
221 
222  member_exprt member(object, component.get_name(), component.type());
223 
224  // recursive call
225  zero_initializer(member, component.type(), source_location, ops);
226  }
227  }
228  else if(final_type.id()==ID_array &&
229  !cpp_is_pod(final_type.subtype()))
230  {
231  const array_typet &array_type=to_array_type(type);
232  const exprt &size_expr=array_type.size();
233 
234  if(size_expr.id()==ID_infinity)
235  return; // don't initialize
236 
237  const mp_integer size =
238  numeric_cast_v<mp_integer>(to_constant_expr(size_expr));
239  CHECK_RETURN(size>=0);
240 
241  exprt::operandst empty_operands;
242  for(mp_integer i=0; i<size; ++i)
243  {
244  index_exprt index(
245  object, from_integer(i, index_type()), array_type.subtype());
246  zero_initializer(index, array_type.subtype(), source_location, ops);
247  }
248  }
249  else if(final_type.id()==ID_union)
250  {
251  const auto &union_type = to_union_type(final_type);
252 
253  if(union_type.is_incomplete())
254  {
255  error().source_location = source_location;
256  error() << "cannot zero-initialize incomplete union" << eom;
257  throw 0;
258  }
259 
260  // Select the largest component for zero-initialization
261  mp_integer max_comp_size=0;
262 
264 
265  for(const auto &component : union_type.components())
266  {
267  assert(component.type().is_not_nil());
268 
269  if(component.type().id()==ID_code)
270  continue;
271 
272  auto component_size_opt = size_of_expr(component.type(), *this);
273 
274  const auto size_int =
275  numeric_cast<mp_integer>(component_size_opt.value_or(nil_exprt()));
276  if(size_int.has_value())
277  {
278  if(*size_int > max_comp_size)
279  {
280  max_comp_size = *size_int;
281  comp=component;
282  }
283  }
284  }
285 
286  if(max_comp_size>0)
287  {
288  const cpp_namet cpp_name(comp.get_base_name(), source_location);
289 
290  exprt member(ID_member);
291  member.copy_to_operands(object);
292  member.set(ID_component_cpp_name, cpp_name);
293  zero_initializer(member, comp.type(), source_location, ops);
294  }
295  }
296  else if(final_type.id()==ID_c_enum)
297  {
298  const unsignedbv_typet enum_type(
299  to_bitvector_type(final_type.subtype()).get_width());
300 
301  exprt zero =
302  typecast_exprt::conditional_cast(from_integer(0, enum_type), type);
304 
305  code_assignt assign;
306  assign.lhs()=object;
307  assign.rhs()=zero;
308  assign.add_source_location()=source_location;
309 
310  typecheck_expr(assign.lhs());
311  assign.lhs().type().set(ID_C_constant, false);
313 
314  typecheck_code(assign);
315  ops.push_back(assign);
316  }
317  else
318  {
319  const auto value = ::zero_initializer(final_type, source_location, *this);
320  if(!value.has_value())
321  {
322  error().source_location = source_location;
323  error() << "cannot zero-initialize '" << to_string(final_type) << "'"
324  << eom;
325  throw 0;
326  }
327 
328  code_assignt assign(object, *value);
329  assign.add_source_location()=source_location;
330 
331  typecheck_expr(assign.lhs());
332  assign.lhs().type().set(ID_C_constant, false);
334 
335  typecheck_code(assign);
336  ops.push_back(assign);
337  }
338 }
c_typecheck_baset::do_initializer
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
Definition: c_typecheck_initializer.cpp:26
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
pointer_offset_size.h
Pointer Logic.
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
typet::subtype
const typet & subtype() const
Definition: type.h:47
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
arith_tools.h
cpp_typecheck_fargst
Definition: cpp_typecheck_fargs.h:22
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
address_of_exprt::object
exprt & object()
Definition: pointer_expr.h:350
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:315
cpp_typecheck_fargs.h
C++ Language Type Checking.
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:116
cpp_typecheck_fargst::operands
exprt::operandst operands
Definition: cpp_typecheck_fargs.h:25
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:43
exprt
Base class for all expressions.
Definition: expr.h:54
cpp_typecheckt::cpp_constructor
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
Definition: cpp_constructor.cpp:22
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
messaget::eom
static eomt eom
Definition: message.h:297
cpp_typecheckt::zero_initializer
void zero_initializer(const exprt &object, const typet &type, const source_locationt &source_location, exprt::operandst &ops)
Definition: cpp_typecheck_initializer.cpp:192
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
array_typet::size
const exprt & size() const
Definition: std_types.h:771
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
cpp_typecheck_fargst::has_object
bool has_object
Definition: cpp_typecheck_fargs.h:24
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
expr_initializer.h
Expression Initialization.
messaget::error
mstreamt & error() const
Definition: message.h:399
already_typechecked_exprt::make_already_typechecked
static void make_already_typechecked(exprt &expr)
Definition: c_typecheck_base.h:292
cpp_typecheckt::convert_initializer
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
Definition: cpp_typecheck_initializer.cpp:24
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:2654
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
cpp_typecheckt::reference_initializer
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:
Definition: cpp_typecheck_conversions.cpp:1547
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:310
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2654
cpp_typecheck_resolvet::wantt::BOTH
@ BOTH
simplify_exprt
Definition: simplify_expr_class.h:74
irept::swap
void swap(irept &irep)
Definition: irep.h:453
cpp_typecheck_fargst::in_use
bool in_use
Definition: cpp_typecheck_fargs.h:24
code_typet
Base type of functions.
Definition: std_types.h:539
cpp_convert_type.h
C++ Language Conversion.
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
cpp_typecheck.h
C++ Language Type Checking.
source_locationt
Definition: source_location.h:19
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:843
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2613
struct_union_typet::componentt
Definition: std_types.h:69
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2254
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:129
array_typet
Arrays with given size.
Definition: std_types.h:763
cpp_typecheckt::typecheck_code
void typecheck_code(codet &) override
Definition: cpp_typecheck_code.cpp:24
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
symbolt::is_type
bool is_type
Definition: symbol.h:61
cpp_typecheckt::has_auto
static bool has_auto(const typet &type)
Definition: cpp_typecheck_compound_type.cpp:67
cpp_typecheckt::implicit_typecast
void implicit_typecast(exprt &expr, const typet &type) override
Definition: cpp_typecheck_conversions.cpp:1480
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
cpp_convert_auto
void cpp_convert_auto(typet &dest, const typet &src, message_handlert &message_handler)
Definition: cpp_convert_type.cpp:352
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:279
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
cpp_typecheckt::to_string
std::string to_string(const typet &) override
Definition: cpp_typecheck.cpp:81
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
index_exprt
Array index operator.
Definition: std_expr.h:1328
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
struct_union_typet::componentt::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:89
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
cpp_typecheckt::resolve
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:83
cpp_namet
Definition: cpp_name.h:17
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
to_cpp_name
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:148
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786