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 `"
35  << symbol.base_name << "'" << 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"
53  << 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());
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(symbol.type.id() == ID_pointer &&
79  symbol.type.subtype().id() == ID_code &&
80  symbol.value.id() == ID_address_of &&
81  symbol.value.op0().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(code_typet::parameterst::const_iterator
93  ait=code_type.parameters().begin();
94  ait!=code_type.parameters().end();
95  ait++)
96  {
97  exprt new_object(ID_new_object, ait->type());
98  new_object.set(ID_C_lvalue, true);
99 
100  if(ait->get(ID_C_base_name)==ID_this)
101  {
102  fargs.has_object = true;
103  new_object.type() = ait->type().subtype();
104  }
105 
106  fargs.operands.push_back(new_object);
107  }
108 
109  exprt resolved_expr=resolve(
110  to_cpp_name(static_cast<irept &>(symbol.value.op0())),
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("to-member") = resolved_expr.op0().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 `"
135  << to_string(symbol.value.type()) << "' to `"
136  << 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("to-member").is_not_nil())
146  symbol.type.add("to-member") = symbol.value.type().find("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());
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);
177  already_typechecked(expr_symbol);
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  for(const auto &component : to_struct_type(final_type).components())
203  {
204  if(component.type().id()==ID_code)
205  continue;
206 
207  if(component.get_bool(ID_is_type))
208  continue;
209 
210  if(component.get_bool(ID_is_static))
211  continue;
212 
213  member_exprt member(object, component.get_name(), component.type());
214 
215  // recursive call
216  zero_initializer(member, component.type(), source_location, ops);
217  }
218  }
219  else if(final_type.id()==ID_array &&
220  !cpp_is_pod(final_type.subtype()))
221  {
222  const array_typet &array_type=to_array_type(type);
223  const exprt &size_expr=array_type.size();
224 
225  if(size_expr.id()==ID_infinity)
226  return; // don't initialize
227 
228  const mp_integer size = numeric_cast_v<mp_integer>(size_expr);
229  CHECK_RETURN(size>=0);
230 
231  exprt::operandst empty_operands;
232  for(mp_integer i=0; i<size; ++i)
233  {
234  index_exprt index(
235  object, from_integer(i, index_type()), array_type.subtype());
236  zero_initializer(index, array_type.subtype(), source_location, ops);
237  }
238  }
239  else if(final_type.id()==ID_union)
240  {
241  // Select the largest component for zero-initialization
242  mp_integer max_comp_size=0;
243 
245 
246  for(const auto &component : to_union_type(final_type).components())
247  {
248  assert(component.type().is_not_nil());
249 
250  if(component.type().id()==ID_code)
251  continue;
252 
253  exprt component_size=size_of_expr(component.type(), *this);
254 
255  mp_integer size_int;
256  if(!to_integer(component_size, size_int))
257  {
258  if(size_int>max_comp_size)
259  {
260  max_comp_size=size_int;
261  comp=component;
262  }
263  }
264  }
265 
266  if(max_comp_size>0)
267  {
268  const cpp_namet cpp_name(comp.get_base_name(), source_location);
269 
270  exprt member(ID_member);
271  member.copy_to_operands(object);
272  member.set(ID_component_cpp_name, cpp_name);
273  zero_initializer(member, comp.type(), source_location, ops);
274  }
275  }
276  else if(final_type.id()==ID_c_enum)
277  {
278  const unsignedbv_typet enum_type(
279  to_bitvector_type(final_type.subtype()).get_width());
280 
281  exprt zero(from_integer(0, enum_type));
282  zero.make_typecast(type);
283  already_typechecked(zero);
284 
285  code_assignt assign;
286  assign.lhs()=object;
287  assign.rhs()=zero;
288  assign.add_source_location()=source_location;
289 
290  typecheck_expr(assign.lhs());
291  assign.lhs().type().set(ID_C_constant, false);
292  already_typechecked(assign.lhs());
293 
294  typecheck_code(assign);
295  ops.push_back(assign);
296  }
297  else if(final_type.id()==ID_incomplete_struct ||
298  final_type.id()==ID_incomplete_union)
299  {
300  error().source_location=source_location;
301  error() << "cannot zero-initialize incomplete compound" << eom;
302  throw 0;
303  }
304  else
305  {
306  const auto value = ::zero_initializer(final_type, source_location, *this);
307  if(!value.has_value())
308  {
309  error().source_location = source_location;
310  error() << "cannot zero-initialize `" << to_string(final_type) << "'"
311  << eom;
312  throw 0;
313  }
314 
315  code_assignt assign(object, *value);
316  assign.add_source_location()=source_location;
317 
318  typecheck_expr(assign.op0());
319  assign.lhs().type().set(ID_C_constant, false);
320  already_typechecked(assign.lhs());
321 
322  typecheck_code(assign);
323  ops.push_back(assign);
324  }
325 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt size_of_expr(const typet &type, const namespacet &ns)
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1223
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:751
bool is_nil() const
Definition: irep.h:172
bool is_not_nil() const
Definition: irep.h:173
static bool has_auto(const typet &type)
exprt & op0()
Definition: expr.h:84
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
exprt::operandst operands
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144
Definition: ai.h:365
void typecheck_expr(exprt &) override
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
exprt value
Initial value of symbol.
Definition: symbol.h:34
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
void typecheck_code(codet &) override
Symbol table entry.
Definition: symbol.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Extract member of struct or union.
Definition: std_expr.h:3890
const irep_idt & get_base_name() const
Definition: std_types.h:142
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
The NIL expression.
Definition: std_expr.h:4461
void cpp_convert_auto(typet &dest, const typet &src)
exprt & rhs()
Definition: std_code.h:274
source_locationt source_location
Definition: message.h:236
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
void typecheck_type(typet &) override
C++ Language Conversion.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
void implicit_typecast(exprt &expr, const typet &type) override
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
mstreamt & error() const
Definition: message.h:386
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
const exprt & size() const
Definition: std_types.h:1010
C++ Language Type Checking.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
Operator to return the address of an object.
Definition: std_expr.h:3255
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
std::vector< exprt > operandst
Definition: expr.h:57
Pointer Logic.
static eomt eom
Definition: message.h:284
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
const source_locationt & source_location() const
Definition: expr.h:228
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
irept & add(const irep_namet &name)
Definition: irep.cpp:305
void swap(irept &irep)
Definition: irep.h:303
source_locationt & add_source_location()
Definition: expr.h:233
Arrays with given size.
Definition: std_types.h:1000
Expression to hold a symbol (variable)
Definition: std_expr.h:143
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
bool is_type
Definition: symbol.h:61
const typet & subtype() const
Definition: type.h:38
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::string to_string(const typet &) override
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
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: ...
bool simplify(exprt &expr, const namespacet &ns)
Array index operator.
Definition: std_expr.h:1595