cprover
cpp_constructor.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_types.h>
16 
17 #include <util/c_types.h>
18 
19 #include "cpp_util.h"
20 
26  const source_locationt &source_location,
27  const exprt &object,
28  const exprt::operandst &operands)
29 {
30  exprt object_tc=object;
31 
32  typecheck_expr(object_tc);
33 
34  elaborate_class_template(object_tc.type());
35 
36  typet tmp_type(follow(object_tc.type()));
37 
38  assert(!is_reference(tmp_type));
39 
40  if(tmp_type.id()==ID_array)
41  {
42  // We allow only one operand and it must be tagged with '#array_ini'.
43  // Note that the operand is an array that is used for copy-initialization.
44  // In the general case, a program is not allowed to use this form of
45  // construct. This way of initializing an array is used internally only.
46  // The purpose of the tag #array_ini is to rule out ill-formed
47  // programs.
48 
49  if(!operands.empty() && !operands.front().get_bool("#array_ini"))
50  {
51  error().source_location=source_location;
52  error() << "bad array initializer" << eom;
53  throw 0;
54  }
55 
56  assert(operands.empty() || operands.size()==1);
57 
58  if(operands.empty() && cpp_is_pod(tmp_type))
59  {
60  codet nil;
61  nil.make_nil();
62  return nil;
63  }
64 
65  const exprt &size_expr=
66  to_array_type(tmp_type).size();
67 
68  if(size_expr.id()=="infinity")
69  {
70  // don't initialize
71  codet nil;
72  nil.make_nil();
73  return nil;
74  }
75 
76  exprt tmp_size=size_expr;
77  make_constant_index(tmp_size);
78 
79  mp_integer s;
80  if(to_integer(tmp_size, s))
81  {
82  error().source_location=source_location;
83  error() << "array size `" << to_string(size_expr)
84  << "' is not a constant" << eom;
85  throw 0;
86  }
87 
88  /*if(cpp_is_pod(tmp_type))
89  {
90  code_expressiont new_code;
91  exprt op_tc=operands.front();
92  typecheck_expr(op_tc);
93  // Override constantness
94  object_tc.type().set("#constant", false);
95  object_tc.set("#lvalue", true);
96  side_effect_exprt assign("assign");
97  assign.add_source_location()=source_location;
98  assign.copy_to_operands(object_tc, op_tc);
99  typecheck_side_effect_assignment(assign);
100  new_code.expression()=assign;
101  return new_code;
102  }
103  else*/
104  {
105  code_blockt new_code;
106 
107  // for each element of the array, call the default constructor
108  for(mp_integer i=0; i < s; ++i)
109  {
110  exprt::operandst tmp_operands;
111 
112  exprt constant=from_integer(i, index_type());
113  constant.add_source_location()=source_location;
114 
115  index_exprt index(object, constant);
116  index.add_source_location()=source_location;
117 
118  if(!operands.empty())
119  {
120  index_exprt operand(operands.front(), constant);
121  operand.add_source_location()=source_location;
122  tmp_operands.push_back(operand);
123  }
124 
125  exprt i_code =
126  cpp_constructor(source_location, index, tmp_operands);
127 
128  if(i_code.is_nil())
129  {
130  new_code.is_nil();
131  break;
132  }
133 
134  new_code.move_to_operands(i_code);
135  }
136  return new_code;
137  }
138  }
139  else if(cpp_is_pod(tmp_type))
140  {
141  code_expressiont new_code;
142  exprt::operandst operands_tc=operands;
143 
144  for(exprt::operandst::iterator
145  it=operands_tc.begin();
146  it!=operands_tc.end();
147  it++)
148  {
149  typecheck_expr(*it);
151  }
152 
153  if(operands_tc.empty())
154  {
155  // a POD is NOT initialized
156  new_code.make_nil();
157  }
158  else if(operands_tc.size()==1)
159  {
160  // Override constantness
161  object_tc.type().set(ID_C_constant, false);
162  object_tc.set(ID_C_lvalue, true);
163  side_effect_exprt assign(ID_assign);
164  assign.add_source_location()=source_location;
165  assign.copy_to_operands(object_tc, operands_tc.front());
167  new_code.expression()=assign;
168  }
169  else
170  {
171  error().source_location=source_location;
172  error() << "initialization of POD requires one argument, "
173  "but got " << operands.size() << eom;
174  throw 0;
175  }
176 
177  return new_code;
178  }
179  else if(tmp_type.id()==ID_union)
180  {
181  UNREACHABLE; // Todo: union
182  }
183  else if(tmp_type.id()==ID_struct)
184  {
185  exprt::operandst operands_tc=operands;
186 
187  for(exprt::operandst::iterator
188  it=operands_tc.begin();
189  it!=operands_tc.end();
190  it++)
191  {
192  typecheck_expr(*it);
194  }
195 
196  const struct_typet &struct_type=
197  to_struct_type(tmp_type);
198 
199  // set most-derived bits
200  code_blockt block;
201  for(std::size_t i=0; i < struct_type.components().size(); i++)
202  {
203  const irept &component=struct_type.components()[i];
204  if(component.get(ID_base_name)!="@most_derived")
205  continue;
206 
207  member_exprt member(object_tc, component.get(ID_name), bool_typet());
208  member.add_source_location()=source_location;
209  member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue));
210 
211  exprt val=false_exprt();
212 
213  if(!component.get_bool("from_base"))
214  val=true_exprt();
215 
216  side_effect_exprt assign(ID_assign);
217  assign.add_source_location()=source_location;
218  assign.move_to_operands(member, val);
220  code_expressiont code_exp(assign);
221  block.move_to_operands(code_exp);
222  }
223 
224  // enter struct scope
225  cpp_save_scopet save_scope(cpp_scopes);
226  cpp_scopes.set_scope(struct_type.get(ID_name));
227 
228  // find name of constructor
229  const struct_typet::componentst &components=
230  struct_type.components();
231 
232  irep_idt constructor_name;
233 
234  for(struct_typet::componentst::const_iterator
235  it=components.begin();
236  it!=components.end();
237  it++)
238  {
239  const typet &type=it->type();
240 
241  if(!it->get_bool(ID_from_base) &&
242  type.id()==ID_code &&
243  type.find(ID_return_type).id()==ID_constructor)
244  {
245  constructor_name=it->get(ID_base_name);
246  break;
247  }
248  }
249 
250  // there is always a constructor for non-PODs
251  assert(constructor_name!="");
252 
253  irept cpp_name(ID_cpp_name);
254  cpp_name.get_sub().push_back(irept(ID_name));
255  cpp_name.get_sub().back().set(ID_identifier, constructor_name);
256  cpp_name.get_sub().back().set(ID_C_source_location, source_location);
257 
258  side_effect_expr_function_callt function_call;
259  function_call.add_source_location()=source_location;
260  function_call.function().swap(static_cast<exprt&>(cpp_name));
261  function_call.arguments().reserve(operands_tc.size());
262 
263  for(exprt::operandst::iterator
264  it=operands_tc.begin();
265  it!=operands_tc.end();
266  it++)
267  function_call.op1().copy_to_operands(*it);
268 
270  assert(function_call.get(ID_statement)==ID_temporary_object);
271 
272  exprt &initializer =
273  static_cast<exprt &>(function_call.add(ID_initializer));
274 
275  assert(initializer.id()==ID_code &&
276  initializer.get(ID_statement)==ID_expression);
277 
279  to_side_effect_expr_function_call(initializer.op0());
280 
281  exprt &tmp_this=func_ini.arguments().front();
282  assert(tmp_this.id()==ID_address_of
283  && tmp_this.op0().id()=="new_object");
284 
285  tmp_this=address_of_exprt(object_tc);
286 
287  if(block.operands().empty())
288  return to_code(initializer);
289  else
290  {
291  block.move_to_operands(initializer);
292  return block;
293  }
294  }
295  else
296  UNREACHABLE;
297 
298  codet nil;
299  nil.make_nil();
300  return nil;
301 }
302 
304  const source_locationt &source_location,
305  const typet &type,
306  const exprt::operandst &ops,
307  exprt &temporary)
308 {
309  // create temporary object
310  exprt tmp_object_expr=exprt(ID_side_effect, type);
311  tmp_object_expr.set(ID_statement, ID_temporary_object);
312  tmp_object_expr.add_source_location()= source_location;
313 
314  exprt new_object(ID_new_object);
315  new_object.add_source_location()=tmp_object_expr.source_location();
316  new_object.set(ID_C_lvalue, true);
317  new_object.type()=tmp_object_expr.type();
318 
319  already_typechecked(new_object);
320 
321  codet new_code =
322  cpp_constructor(source_location, new_object, ops);
323 
324  if(new_code.is_not_nil())
325  {
326  if(new_code.get(ID_statement)==ID_assign)
327  tmp_object_expr.move_to_operands(new_code.op1());
328  else
329  tmp_object_expr.add(ID_initializer)=new_code;
330  }
331 
332  temporary.swap(tmp_object_expr);
333 }
334 
336  const source_locationt &source_location,
337  const typet &type,
338  const exprt &op,
339  exprt &temporary)
340 {
341  exprt::operandst ops;
342  ops.push_back(op);
343  new_temporary(source_location, type, ops, temporary);
344 }
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1392
The type of an expression.
Definition: type.h:22
void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:102
bool is_not_nil() const
Definition: irep.h:103
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
void add_implicit_dereference(exprt &expr)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
An expression statement.
Definition: std_code.h:1188
virtual void typecheck_expr(exprt &expr)
subt & get_sub()
Definition: irep.h:245
Extract member of struct or union.
Definition: std_expr.h:3871
const irep_idt & id() const
Definition: irep.h:189
void elaborate_class_template(const typet &type)
elaborate class template instances
The boolean constant true.
Definition: std_expr.h:4488
source_locationt source_location
Definition: message.h:214
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
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
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
void typecheck_side_effect_assignment(side_effect_exprt &expr)
Operator to return the address of an object.
Definition: std_expr.h:3170
The boolean constant false.
Definition: std_expr.h:4499
std::vector< exprt > operandst
Definition: expr.h:45
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
A function call side effect.
Definition: std_code.h:1352
API to type classes.
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 source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
const exprt & expression() const
Definition: std_code.h:1201
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual std::string to_string(const typet &type)
exprt::operandst & arguments()
Definition: std_code.h:1371
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
A statement in a programming language.
Definition: std_code.h:21
An expression containing a side effect.
Definition: std_code.h:1238
operandst & operands()
Definition: expr.h:66
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)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
array index operator
Definition: std_expr.h:1462
cpp_scopest cpp_scopes