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/std_expr.h>
16 
18 #include <util/c_types.h>
19 #include <ansi-c/c_sizeof.h>
20 
21 #include "cpp_util.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 `"
37  << symbol.base_name << "'" << 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"
55  << eom;
56  throw 0;
57  }
58 
59  // done
60  return;
61  }
62 
63  // we do have an initializer
64 
65  if(is_reference(symbol.type))
66  {
67  typecheck_expr(symbol.value);
68  reference_initializer(symbol.value, symbol.type);
69  }
70  else if(cpp_is_pod(symbol.type))
71  {
72  if(symbol.type.id() == ID_pointer &&
73  symbol.type.subtype().id() == ID_code &&
74  symbol.value.id() == ID_address_of &&
75  symbol.value.op0().id() == ID_cpp_name)
76  {
77  // initialization of a function pointer with
78  // the address of a function: use pointer type information
79  // for the sake of overload resolution
80 
82  fargs.in_use = true;
83 
84  const code_typet &code_type=to_code_type(symbol.type.subtype());
85 
86  for(code_typet::parameterst::const_iterator
87  ait=code_type.parameters().begin();
88  ait!=code_type.parameters().end();
89  ait++)
90  {
91  exprt new_object("new_object");
92  new_object.set(ID_C_lvalue, true);
93  new_object.type() = ait->type();
94 
95  if(ait->get(ID_C_base_name)==ID_this)
96  {
97  fargs.has_object = true;
98  new_object.type() = ait->type().subtype();
99  }
100 
101  fargs.operands.push_back(new_object);
102  }
103 
104  exprt resolved_expr=resolve(
105  to_cpp_name(static_cast<irept &>(symbol.value.op0())),
107 
108  assert(symbol.type.subtype() == resolved_expr.type());
109 
110  if(resolved_expr.id()==ID_symbol)
111  {
112  symbol.value=
113  address_of_exprt(resolved_expr);
114  }
115  else if(resolved_expr.id()==ID_member)
116  {
117  symbol.value =
119  lookup(resolved_expr.get(ID_component_name)).symbol_expr());
120 
121  symbol.value.type().add("to-member") = resolved_expr.op0().type();
122  }
123  else
124  assert(false);
125 
126  if(symbol.type != symbol.value.type())
127  {
128  error().source_location=symbol.location;
129  error() << "conversion from `"
130  << to_string(symbol.value.type()) << "' to `"
131  << to_string(symbol.type) << "' " << eom;
132  throw 0;
133  }
134 
135  return;
136  }
137 
138  typecheck_expr(symbol.value);
139 
140  if(symbol.value.id()==ID_initializer_list ||
141  symbol.value.id()==ID_string_constant)
142  {
143  do_initializer(symbol.value, symbol.type, true);
144 
145  if(symbol.type.find(ID_size).is_nil())
146  symbol.type=symbol.value.type();
147  }
148  else
149  implicit_typecast(symbol.value, symbol.type);
150 
151  #if 0
152  simplify_exprt simplify(*this);
153  exprt tmp_value = symbol.value;
154  if(!simplify.simplify(tmp_value))
155  symbol.value.swap(tmp_value);
156  #endif
157  }
158  else
159  {
160  // we need a constructor
161 
162  symbol_exprt expr_symbol(symbol.name, symbol.type);
163  already_typechecked(expr_symbol);
164 
165  exprt::operandst ops;
166  ops.push_back(symbol.value);
167 
168  symbol.value = cpp_constructor(
169  symbol.value.source_location(),
170  expr_symbol,
171  ops);
172  }
173 }
174 
176  const exprt &object,
177  const typet &type,
178  const source_locationt &source_location,
179  exprt::operandst &ops)
180 {
181  const typet &final_type=follow(type);
182 
183  if(final_type.id()==ID_struct)
184  {
185  forall_irep(cit, final_type.find(ID_components).get_sub())
186  {
187  const exprt &component=static_cast<const exprt &>(*cit);
188 
189  if(component.type().id()==ID_code)
190  continue;
191 
192  if(component.get_bool(ID_is_type))
193  continue;
194 
195  if(component.get_bool(ID_is_static))
196  continue;
197 
198  exprt member(ID_member);
199  member.copy_to_operands(object);
200  member.set(ID_component_name, component.get(ID_name));
201 
202  // recursive call
203  zero_initializer(member, component.type(), source_location, ops);
204  }
205  }
206  else if(final_type.id()==ID_array &&
207  !cpp_is_pod(final_type.subtype()))
208  {
209  const array_typet &array_type=to_array_type(type);
210  const exprt &size_expr=array_type.size();
211 
212  if(size_expr.id()==ID_infinity)
213  return; // don't initialize
214 
215  mp_integer size;
216 
217  bool to_int=to_integer(size_expr, size);
218  assert(!to_int);
219  assert(size>=0);
220 
221  exprt::operandst empty_operands;
222  for(mp_integer i=0; i<size; ++i)
223  {
224  exprt index(ID_index);
225  index.copy_to_operands(object, from_integer(i, index_type()));
226  zero_initializer(index, array_type.subtype(), source_location, ops);
227  }
228  }
229  else if(final_type.id()==ID_union)
230  {
231  c_sizeoft c_sizeof(*this);
232 
233  // Select the largest component for zero-initialization
234  mp_integer max_comp_size=0;
235 
236  exprt comp=nil_exprt();
237 
238  forall_irep(it, final_type.find(ID_components).get_sub())
239  {
240  const exprt &component=static_cast<const exprt &>(*it);
241 
242  assert(component.type().is_not_nil());
243 
244  if(component.type().id()==ID_code)
245  continue;
246 
247  exprt component_size=c_sizeof(component.type());
248 
249  mp_integer size_int;
250  if(!to_integer(component_size, size_int))
251  {
252  if(size_int>max_comp_size)
253  {
254  max_comp_size=size_int;
255  comp=component;
256  }
257  }
258  }
259 
260  if(max_comp_size>0)
261  {
262  irept name(ID_name);
263  name.set(ID_identifier, comp.get(ID_base_name));
264  name.set(ID_C_source_location, source_location);
265 
266  cpp_namet cpp_name;
267  cpp_name.move_to_sub(name);
268 
269  exprt member(ID_member);
270  member.copy_to_operands(object);
271  member.set(ID_component_cpp_name, cpp_name);
272  zero_initializer(member, comp.type(), source_location, ops);
273  }
274  }
275  else if(final_type.id()==ID_c_enum)
276  {
277  typet enum_type(ID_unsignedbv);
278  enum_type.add(ID_width)=final_type.find(ID_width);
279 
280  exprt zero(from_integer(0, enum_type));
281  zero.make_typecast(type);
282  already_typechecked(zero);
283 
284  code_assignt assign;
285  assign.lhs()=object;
286  assign.rhs()=zero;
287  assign.add_source_location()=source_location;
288 
289  typecheck_expr(assign.lhs());
290  assign.lhs().type().set(ID_C_constant, false);
291  already_typechecked(assign.lhs());
292 
293  typecheck_code(assign);
294  ops.push_back(assign);
295  }
296  else if(final_type.id()==ID_incomplete_struct ||
297  final_type.id()==ID_incomplete_union)
298  {
299  error().source_location=source_location;
300  error() << "cannot zero-initialize incomplete compound" << eom;
301  throw 0;
302  }
303  else
304  {
305  exprt value=
307  final_type, source_location, *this, get_message_handler());
308 
309  code_assignt assign;
310  assign.lhs()=object;
311  assign.rhs()=value;
312  assign.add_source_location()=source_location;
313 
314  typecheck_expr(assign.op0());
315  assign.lhs().type().set(ID_C_constant, false);
316  already_typechecked(assign.lhs());
317 
318  typecheck_code(assign);
319  ops.push_back(assign);
320  }
321 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
BigInt mp_integer
Definition: mp_arith.h:19
Linking: Zero Initialization.
void typecheck_type(typet &type)
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
exprt & op0()
Definition: expr.h:84
void move_to_sub(irept &irep)
Definition: irep.cpp:204
exprt::operandst operands
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
cpp_namet & to_cpp_name(irept &cpp_name)
Definition: cpp_name.h:143
Definition: ai.h:342
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:40
typet & type()
Definition: expr.h:60
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:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
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
const irep_idt & id() const
Definition: irep.h:189
exprt c_sizeof(const typet &src, const namespacet &ns)
Definition: c_sizeof.cpp:303
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
exprt & lhs()
Definition: std_code.h:157
The NIL expression.
Definition: std_expr.h:3764
exprt & rhs()
Definition: std_code.h:162
source_locationt source_location
Definition: message.h:175
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
API to expression classes.
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
void convert_initializer(symbolt &symbol)
Initialize an object with a value.
const exprt & size() const
Definition: std_types.h:915
Base class for tree-like data structures with sharing.
Definition: irep.h:87
C++ Language Type Checking.
bitvector_typet index_type()
Definition: c_types.cpp:15
Operator to return the address of an object.
Definition: std_expr.h:2593
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:49
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
message_handlert & get_message_handler()
Definition: message.h:127
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const source_locationt & source_location() const
Definition: expr.h:142
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual std::string to_string(const typet &type)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
arrays with given size
Definition: std_types.h:901
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
bool is_type
Definition: symbol.h:66
const typet & subtype() const
Definition: type.h:31
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:90
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)
Assignment.
Definition: std_code.h:144
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:62