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(ID_C_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  return {};
60 
61  const exprt &size_expr=
62  to_array_type(tmp_type).size();
63 
64  if(size_expr.id() == ID_infinity)
65  return {}; // don't initialize
66 
67  exprt tmp_size=size_expr;
68  make_constant_index(tmp_size);
69 
70  mp_integer s;
71  if(to_integer(tmp_size, s))
72  {
73  error().source_location=source_location;
74  error() << "array size `" << to_string(size_expr)
75  << "' is not a constant" << eom;
76  throw 0;
77  }
78 
79  /*if(cpp_is_pod(tmp_type))
80  {
81  code_expressiont new_code;
82  exprt op_tc=operands.front();
83  typecheck_expr(op_tc);
84  // Override constantness
85  object_tc.type().set("ID_C_constant", false);
86  object_tc.set("ID_C_lvalue", true);
87  side_effect_exprt assign(ID_assign);
88  assign.add_source_location()=source_location;
89  assign.copy_to_operands(object_tc, op_tc);
90  typecheck_side_effect_assignment(assign);
91  new_code.expression()=assign;
92  return new_code;
93  }
94  else*/
95  {
96  code_blockt new_code;
97 
98  // for each element of the array, call the default constructor
99  for(mp_integer i=0; i < s; ++i)
100  {
101  exprt::operandst tmp_operands;
102 
103  exprt constant=from_integer(i, index_type());
104  constant.add_source_location()=source_location;
105 
106  index_exprt index(object, constant);
107  index.add_source_location()=source_location;
108 
109  if(!operands.empty())
110  {
111  index_exprt operand(operands.front(), constant);
112  operand.add_source_location()=source_location;
113  tmp_operands.push_back(operand);
114  }
115 
116  auto i_code = cpp_constructor(source_location, index, tmp_operands);
117 
118  if(i_code.has_value())
119  new_code.add(std::move(i_code.value()));
120  }
121  return std::move(new_code);
122  }
123  }
124  else if(cpp_is_pod(tmp_type))
125  {
126  exprt::operandst operands_tc=operands;
127 
128  for(auto &op : operands_tc)
129  {
130  typecheck_expr(op);
132  }
133 
134  if(operands_tc.empty())
135  {
136  // a POD is NOT initialized
137  return {};
138  }
139  else if(operands_tc.size()==1)
140  {
141  // Override constantness
142  object_tc.type().set(ID_C_constant, false);
143  object_tc.set(ID_C_lvalue, true);
144  side_effect_exprt assign(ID_assign, typet(), source_location);
145  assign.copy_to_operands(object_tc, operands_tc.front());
147  code_expressiont new_code;
148  new_code.expression()=assign;
149  return std::move(new_code);
150  }
151  else
152  {
153  error().source_location=source_location;
154  error() << "initialization of POD requires one argument, "
155  "but got " << operands.size() << eom;
156  throw 0;
157  }
158  }
159  else if(tmp_type.id()==ID_union)
160  {
161  UNREACHABLE; // Todo: union
162  }
163  else if(tmp_type.id()==ID_struct)
164  {
165  exprt::operandst operands_tc=operands;
166 
167  for(auto &op : operands_tc)
168  {
169  typecheck_expr(op);
171  }
172 
173  const struct_typet &struct_type=
174  to_struct_type(tmp_type);
175 
176  // set most-derived bits
177  code_blockt block;
178  for(const auto &component : struct_type.components())
179  {
180  if(component.get_base_name() != "@most_derived")
181  continue;
182 
183  member_exprt member(object_tc, component.get_name(), bool_typet());
184  member.add_source_location()=source_location;
185  member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue));
186 
187  exprt val=false_exprt();
188 
189  if(!component.get_bool(ID_from_base))
190  val=true_exprt();
191 
192  side_effect_exprt assign(ID_assign, typet(), source_location);
193  assign.move_to_operands(member, val);
195  block.add(std::move(code_expressiont(assign)));
196  }
197 
198  // enter struct scope
199  cpp_save_scopet save_scope(cpp_scopes);
200  cpp_scopes.set_scope(struct_type.get(ID_name));
201 
202  // find name of constructor
203  const struct_typet::componentst &components=
204  struct_type.components();
205 
206  irep_idt constructor_name;
207 
208  for(const auto &c : components)
209  {
210  const typet &type = c.type();
211 
212  if(
213  !c.get_bool(ID_from_base) && type.id() == ID_code &&
214  to_code_type(type).return_type().id() == ID_constructor)
215  {
216  constructor_name = c.get_base_name();
217  break;
218  }
219  }
220 
221  // there is always a constructor for non-PODs
222  assert(constructor_name!="");
223 
224  side_effect_expr_function_callt function_call(
225  cpp_namet(constructor_name, source_location).as_expr(),
226  operands_tc);
227 
228  function_call.add_source_location()=source_location;
229 
231  assert(function_call.get(ID_statement)==ID_temporary_object);
232 
233  exprt &initializer =
234  static_cast<exprt &>(function_call.add(ID_initializer));
235 
236  assert(initializer.id()==ID_code &&
237  initializer.get(ID_statement)==ID_expression);
238 
240  to_side_effect_expr_function_call(initializer.op0());
241 
242  exprt &tmp_this=func_ini.arguments().front();
244  to_address_of_expr(tmp_this).object().id() == ID_new_object,
245  "expected new_object operand in address_of expression");
246 
247  tmp_this=address_of_exprt(object_tc);
248 
249  const auto &initializer_code=to_code(initializer);
250 
251  if(block.statements().empty())
252  return initializer_code;
253  else
254  {
255  block.add(initializer_code);
256  return std::move(block);
257  }
258  }
259  else
260  UNREACHABLE;
261 
262  return {};
263 }
264 
266  const source_locationt &source_location,
267  const typet &type,
268  const exprt::operandst &ops,
269  exprt &temporary)
270 {
271  // create temporary object
272  exprt tmp_object_expr=exprt(ID_side_effect, type);
273  tmp_object_expr.set(ID_statement, ID_temporary_object);
274  tmp_object_expr.add_source_location()= source_location;
275 
276  exprt new_object(ID_new_object);
277  new_object.add_source_location()=tmp_object_expr.source_location();
278  new_object.set(ID_C_lvalue, true);
279  new_object.type()=tmp_object_expr.type();
280 
281  already_typechecked(new_object);
282 
283  auto new_code = cpp_constructor(source_location, new_object, ops);
284 
285  if(new_code.has_value())
286  {
287  if(new_code->get_statement() == ID_assign)
288  tmp_object_expr.move_to_operands(new_code->op1());
289  else
290  tmp_object_expr.add(ID_initializer) = *new_code;
291  }
292 
293  temporary.swap(tmp_object_expr);
294 }
295 
297  const source_locationt &source_location,
298  const typet &type,
299  const exprt &op,
300  exprt &temporary)
301 {
302  exprt::operandst ops;
303  ops.push_back(op);
304  new_temporary(source_location, type, ops, temporary);
305 }
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1775
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
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
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt&#39;s operands.
Definition: expr.h:123
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
code_operandst & statements()
Definition: std_code.h:159
std::vector< componentt > componentst
Definition: std_types.h:203
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
void typecheck_expr(exprt &) override
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
The Boolean type.
Definition: std_types.h:28
Structure type, corresponds to C style structs.
Definition: std_types.h:276
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
codet representation of an expression statement.
Definition: std_code.h:1504
void typecheck_side_effect_assignment(side_effect_exprt &) override
Extract member of struct or union.
Definition: std_expr.h:3890
const irep_idt & id() const
Definition: irep.h:259
void elaborate_class_template(const typet &type)
elaborate class template instances
void add(const codet &code)
Definition: std_code.h:189
The Boolean constant true.
Definition: std_expr.h:4443
source_locationt source_location
Definition: message.h:236
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
nonstd::optional< T > optionalt
Definition: optional.h:35
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
mstreamt & error() const
Definition: message.h:386
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
The Boolean constant false.
Definition: std_expr.h:4452
std::vector< exprt > operandst
Definition: expr.h:57
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
static eomt eom
Definition: message.h:284
Pre-defined types.
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 source_locationt & source_location() const
Definition: expr.h:228
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const exprt & expression() const
Definition: std_code.h:1518
virtual void make_constant_index(exprt &expr)
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
A codet representing sequential composition of program statements.
Definition: std_code.h:150
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
An expression containing a side effect.
Definition: std_code.h:1560
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
std::string to_string(const typet &) override
const typet & return_type() const
Definition: std_types.h:883
void add_implicit_dereference(exprt &)
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
Array index operator.
Definition: std_expr.h:1595
cpp_scopest cpp_scopes