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 
25  const source_locationt &source_location,
26  const exprt &object,
27  const exprt::operandst &operands)
28 {
29  exprt object_tc=object;
30 
31  typecheck_expr(object_tc);
32 
33  elaborate_class_template(object_tc.type());
34 
35  typet tmp_type(object_tc.type());
36  follow_symbol(tmp_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 allow 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  codet new_code(ID_block);
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  exprt index(ID_index);
116  index.copy_to_operands(object);
117  index.copy_to_operands(constant);
118  index.add_source_location()=source_location;
119 
120  if(!operands.empty())
121  {
122  exprt operand(ID_index);
123  operand.copy_to_operands(operands.front());
124  operand.copy_to_operands(constant);
125  operand.add_source_location()=source_location;
126  tmp_operands.push_back(operand);
127  }
128 
129  exprt i_code =
130  cpp_constructor(source_location, index, tmp_operands);
131 
132  if(i_code.is_nil())
133  {
134  new_code.is_nil();
135  break;
136  }
137 
138  new_code.move_to_operands(i_code);
139  }
140  return new_code;
141  }
142  }
143  else if(cpp_is_pod(tmp_type))
144  {
145  code_expressiont new_code;
146  exprt::operandst operands_tc=operands;
147 
148  for(exprt::operandst::iterator
149  it=operands_tc.begin();
150  it!=operands_tc.end();
151  it++)
152  {
153  typecheck_expr(*it);
155  }
156 
157  if(operands_tc.empty())
158  {
159  // a POD is NOT initialized
160  new_code.make_nil();
161  }
162  else if(operands_tc.size()==1)
163  {
164  // Override constantness
165  object_tc.type().set(ID_C_constant, false);
166  object_tc.set(ID_C_lvalue, true);
167  side_effect_exprt assign(ID_assign);
168  assign.add_source_location()=source_location;
169  assign.copy_to_operands(object_tc, operands_tc.front());
171  new_code.expression()=assign;
172  }
173  else
174  {
175  error().source_location=source_location;
176  error() << "initialization of POD requires one argument, "
177  "but got " << operands.size() << eom;
178  throw 0;
179  }
180 
181  return new_code;
182  }
183  else if(tmp_type.id()==ID_union)
184  {
185  assert(0); // Todo: union
186  }
187  else if(tmp_type.id()==ID_struct)
188  {
189  exprt::operandst operands_tc=operands;
190 
191  for(exprt::operandst::iterator
192  it=operands_tc.begin();
193  it!=operands_tc.end();
194  it++)
195  {
196  typecheck_expr(*it);
198  }
199 
200  const struct_typet &struct_type=
201  to_struct_type(tmp_type);
202 
203  // set most-derived bits
204  codet block(ID_block);
205  for(std::size_t i=0; i < struct_type.components().size(); i++)
206  {
207  const irept &component=struct_type.components()[i];
208  if(component.get(ID_base_name)!="@most_derived")
209  continue;
210 
211  exprt member(ID_member, bool_typet());
212  member.set(ID_component_name, component.get(ID_name));
213  member.copy_to_operands(object_tc);
214  member.add_source_location()=source_location;
215  member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue));
216 
217  exprt val=false_exprt();
218 
219  if(!component.get_bool("from_base"))
220  val=true_exprt();
221 
222  side_effect_exprt assign(ID_assign);
223  assign.add_source_location()=source_location;
224  assign.move_to_operands(member, val);
226  code_expressiont code_exp;
227  code_exp.expression()=assign;
228  block.move_to_operands(code_exp);
229  }
230 
231  // enter struct scope
232  cpp_save_scopet save_scope(cpp_scopes);
233  cpp_scopes.set_scope(struct_type.get(ID_name));
234 
235  // find name of constructor
236  const struct_typet::componentst &components=
237  struct_type.components();
238 
239  irep_idt constructor_name;
240 
241  for(struct_typet::componentst::const_iterator
242  it=components.begin();
243  it!=components.end();
244  it++)
245  {
246  const typet &type=it->type();
247 
248  if(!it->get_bool(ID_from_base) &&
249  type.id()==ID_code &&
250  type.find(ID_return_type).id()==ID_constructor)
251  {
252  constructor_name=it->get(ID_base_name);
253  break;
254  }
255  }
256 
257  // there is always a constructor for non-PODs
258  assert(constructor_name!="");
259 
260  irept cpp_name(ID_cpp_name);
261  cpp_name.get_sub().push_back(irept(ID_name));
262  cpp_name.get_sub().back().set(ID_identifier, constructor_name);
263  cpp_name.get_sub().back().set(ID_C_source_location, source_location);
264 
265  side_effect_expr_function_callt function_call;
266  function_call.add_source_location()=source_location;
267  function_call.function().swap(static_cast<exprt&>(cpp_name));
268  function_call.arguments().reserve(operands_tc.size());
269 
270  for(exprt::operandst::iterator
271  it=operands_tc.begin();
272  it!=operands_tc.end();
273  it++)
274  function_call.op1().copy_to_operands(*it);
275 
277  assert(function_call.get(ID_statement)==ID_temporary_object);
278 
279  exprt &initializer =
280  static_cast<exprt &>(function_call.add(ID_initializer));
281 
282  assert(initializer.id()==ID_code &&
283  initializer.get(ID_statement)==ID_expression);
284 
286  to_side_effect_expr_function_call(initializer.op0());
287 
288  exprt &tmp_this=func_ini.arguments().front();
289  assert(tmp_this.id()==ID_address_of
290  && tmp_this.op0().id()=="new_object");
291 
292  tmp_this=address_of_exprt(object_tc);
293 
294  if(block.operands().empty())
295  return to_code(initializer);
296  else
297  {
298  block.move_to_operands(initializer);
299  return block;
300  }
301  }
302  else
303  assert(false);
304 
305  codet nil;
306  nil.make_nil();
307  return nil;
308 }
309 
311  const source_locationt &source_location,
312  const typet &type,
313  const exprt::operandst &ops,
314  exprt &temporary)
315 {
316  // create temporary object
317  exprt tmp_object_expr=exprt(ID_side_effect, type);
318  tmp_object_expr.set(ID_statement, ID_temporary_object);
319  tmp_object_expr.add_source_location()= source_location;
320 
321  exprt new_object(ID_new_object);
322  new_object.add_source_location()=tmp_object_expr.source_location();
323  new_object.set(ID_C_lvalue, true);
324  new_object.type()=tmp_object_expr.type();
325 
326  already_typechecked(new_object);
327 
328  codet new_code =
329  cpp_constructor(source_location, new_object, ops);
330 
331  if(new_code.is_not_nil())
332  {
333  if(new_code.get(ID_statement)==ID_assign)
334  tmp_object_expr.move_to_operands(new_code.op1());
335  else
336  tmp_object_expr.add(ID_initializer)=new_code;
337  }
338 
339  temporary.swap(tmp_object_expr);
340 }
341 
343  const source_locationt &source_location,
344  const typet &type,
345  const exprt &op,
346  exprt &temporary)
347 {
348  exprt::operandst ops;
349  ops.push_back(op);
350  new_temporary(source_location, type, ops, temporary);
351 }
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1083
The type of an expression.
Definition: type.h:20
void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
bool is_not_nil() const
Definition: irep.h:104
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:61
std::vector< componentt > componentst
Definition: std_types.h:240
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Structure type.
Definition: std_types.h:296
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
An expression statement.
Definition: std_code.h:957
virtual void typecheck_expr(exprt &expr)
subt & get_sub()
Definition: irep.h:245
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
void elaborate_class_template(const typet &type)
elaborate class template instances
The boolean constant true.
Definition: std_expr.h:3742
source_locationt source_location
Definition: message.h:175
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:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
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
void typecheck_side_effect_assignment(side_effect_exprt &expr)
Operator to return the address of an object.
Definition: std_expr.h:2593
The boolean constant false.
Definition: std_expr.h:3753
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
A function call side effect.
Definition: std_code.h:1052
void follow_symbol(irept &irep) const
Definition: namespace.cpp:43
API to type classes.
Base class for all expressions.
Definition: expr.h:46
const source_locationt & source_location() const
Definition: expr.h:142
const exprt & expression() const
Definition: std_code.h:970
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:1071
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
A statement in a programming language.
Definition: std_code.h:19
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
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
cpp_scopest cpp_scopes