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("new_object");
98  new_object.set(ID_C_lvalue, true);
99  new_object.type() = ait->type();
100 
101  if(ait->get(ID_C_base_name)==ID_this)
102  {
103  fargs.has_object = true;
104  new_object.type() = ait->type().subtype();
105  }
106 
107  fargs.operands.push_back(new_object);
108  }
109 
110  exprt resolved_expr=resolve(
111  to_cpp_name(static_cast<irept &>(symbol.value.op0())),
113 
114  assert(symbol.type.subtype() == resolved_expr.type());
115 
116  if(resolved_expr.id()==ID_symbol)
117  {
118  symbol.value=
119  address_of_exprt(resolved_expr);
120  }
121  else if(resolved_expr.id()==ID_member)
122  {
123  symbol.value =
125  lookup(resolved_expr.get(ID_component_name)).symbol_expr());
126 
127  symbol.value.type().add("to-member") = resolved_expr.op0().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 `"
136  << to_string(symbol.value.type()) << "' to `"
137  << to_string(symbol.type) << "' " << eom;
138  throw 0;
139  }
140 
141  return;
142  }
143 
144  typecheck_expr(symbol.value);
145 
146  if(symbol.value.type().find("to-member").is_not_nil())
147  symbol.type.add("to-member") = symbol.value.type().find("to-member");
148 
149  if(symbol.value.id()==ID_initializer_list ||
150  symbol.value.id()==ID_string_constant)
151  {
152  do_initializer(symbol.value, symbol.type, true);
153 
154  if(symbol.type.find(ID_size).is_nil())
155  symbol.type=symbol.value.type();
156  }
157  else if(has_auto(symbol.type))
158  {
159  cpp_convert_auto(symbol.type, symbol.value.type());
160  typecheck_type(symbol.type);
161  implicit_typecast(symbol.value, symbol.type);
162  }
163  else
164  implicit_typecast(symbol.value, symbol.type);
165 
166  #if 0
167  simplify_exprt simplify(*this);
168  exprt tmp_value = symbol.value;
169  if(!simplify.simplify(tmp_value))
170  symbol.value.swap(tmp_value);
171  #endif
172  }
173  else
174  {
175  // we need a constructor
176 
177  symbol_exprt expr_symbol(symbol.name, symbol.type);
178  already_typechecked(expr_symbol);
179 
180  exprt::operandst ops;
181  ops.push_back(symbol.value);
182 
183  symbol.value = cpp_constructor(
184  symbol.value.source_location(),
185  expr_symbol,
186  ops);
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  forall_irep(cit, final_type.find(ID_components).get_sub())
201  {
202  const exprt &component=static_cast<const exprt &>(*cit);
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(ID_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  mp_integer size;
229 
230  bool to_int=to_integer(size_expr, size);
231  CHECK_RETURN(!to_int);
232  CHECK_RETURN(size>=0);
233 
234  exprt::operandst empty_operands;
235  for(mp_integer i=0; i<size; ++i)
236  {
237  index_exprt index(
238  object, from_integer(i, index_type()), array_type.subtype());
239  zero_initializer(index, array_type.subtype(), source_location, ops);
240  }
241  }
242  else if(final_type.id()==ID_union)
243  {
244  // Select the largest component for zero-initialization
245  mp_integer max_comp_size=0;
246 
247  exprt comp=nil_exprt();
248 
249  forall_irep(it, final_type.find(ID_components).get_sub())
250  {
251  const exprt &component=static_cast<const exprt &>(*it);
252 
253  assert(component.type().is_not_nil());
254 
255  if(component.type().id()==ID_code)
256  continue;
257 
258  exprt component_size=size_of_expr(component.type(), *this);
259 
260  mp_integer size_int;
261  if(!to_integer(component_size, size_int))
262  {
263  if(size_int>max_comp_size)
264  {
265  max_comp_size=size_int;
266  comp=component;
267  }
268  }
269  }
270 
271  if(max_comp_size>0)
272  {
273  irept name(ID_name);
274  name.set(ID_identifier, comp.get(ID_base_name));
275  name.set(ID_C_source_location, source_location);
276 
277  cpp_namet cpp_name;
278  cpp_name.move_to_sub(name);
279 
280  exprt member(ID_member);
281  member.copy_to_operands(object);
282  member.set(ID_component_cpp_name, cpp_name);
283  zero_initializer(member, comp.type(), source_location, ops);
284  }
285  }
286  else if(final_type.id()==ID_c_enum)
287  {
288  const unsignedbv_typet enum_type(
289  to_bitvector_type(final_type.subtype()).get_width());
290 
291  exprt zero(from_integer(0, enum_type));
292  zero.make_typecast(type);
293  already_typechecked(zero);
294 
295  code_assignt assign;
296  assign.lhs()=object;
297  assign.rhs()=zero;
298  assign.add_source_location()=source_location;
299 
300  typecheck_expr(assign.lhs());
301  assign.lhs().type().set(ID_C_constant, false);
302  already_typechecked(assign.lhs());
303 
304  typecheck_code(assign);
305  ops.push_back(assign);
306  }
307  else if(final_type.id()==ID_incomplete_struct ||
308  final_type.id()==ID_incomplete_union)
309  {
310  error().source_location=source_location;
311  error() << "cannot zero-initialize incomplete compound" << eom;
312  throw 0;
313  }
314  else
315  {
316  exprt value=
318  final_type, source_location, *this, get_message_handler());
319 
320  code_assignt assign;
321  assign.lhs()=object;
322  assign.rhs()=value;
323  assign.add_source_location()=source_location;
324 
325  typecheck_expr(assign.op0());
326  assign.lhs().type().set(ID_C_constant, false);
327  already_typechecked(assign.lhs());
328 
329  typecheck_code(assign);
330  ops.push_back(assign);
331  }
332 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
exprt size_of_expr(const typet &type, const namespacet &ns)
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
BigInt mp_integer
Definition: mp_arith.h:22
void typecheck_type(typet &type)
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
static bool has_auto(const typet &type)
exprt & op0()
Definition: expr.h:72
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1150
void move_to_sub(irept &irep)
Definition: irep.cpp:204
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
exprt::operandst operands
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:144
Definition: ai.h:377
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
virtual void typecheck_code(codet &code)
exprt value
Initial value of symbol.
Definition: symbol.h:37
typet & type()
Definition: expr.h:56
virtual void implicit_typecast(exprt &expr, const typet &type)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
virtual void typecheck_expr(exprt &expr)
subt & get_sub()
Definition: irep.h:245
Extract member of struct or union.
Definition: std_expr.h:3871
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
The NIL expression.
Definition: std_expr.h:4510
void cpp_convert_auto(typet &dest, const typet &src)
exprt & rhs()
Definition: std_code.h:213
source_locationt source_location
Definition: message.h:214
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
C++ Language Conversion.
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
const exprt & size() const
Definition: std_types.h:1014
Base class for tree-like data structures with sharing.
Definition: irep.h:86
C++ Language Type Checking.
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: std_expr.h:3170
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:87
std::vector< exprt > operandst
Definition: expr.h:45
Pointer Logic.
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
message_handlert & get_message_handler()
Definition: message.h:153
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual std::string to_string(const typet &type)
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:130
arrays with given size
Definition: std_types.h:1004
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
bool is_type
Definition: symbol.h:63
const typet & subtype() const
Definition: type.h:33
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
codet cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
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)
#define forall_irep(it, irep)
Definition: irep.h:61
array index operator
Definition: std_expr.h:1462