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