CBMC
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/c_types.h>
16 #include <util/pointer_expr.h>
17 
22 std::optional<codet> cpp_typecheckt::cpp_constructor(
23  const source_locationt &source_location,
24  const exprt &object,
25  const exprt::operandst &operands)
26 {
27  exprt object_tc=object;
28 
29  typecheck_expr(object_tc);
30 
31  elaborate_class_template(object_tc.type());
32 
33  CHECK_RETURN(!is_reference(object_tc.type()));
34 
35  if(object_tc.type().id() == ID_array)
36  {
37  // We allow only one operand and it must be tagged with '#array_ini'.
38  // Note that the operand is an array that is used for copy-initialization.
39  // In the general case, a program is not allowed to use this form of
40  // construct. This way of initializing an array is used internally only.
41  // The purpose of the tag #array_ini is to rule out ill-formed
42  // programs.
43 
44  if(!operands.empty() && !operands.front().get_bool(ID_C_array_ini))
45  {
46  error().source_location=source_location;
47  error() << "bad array initializer" << eom;
48  throw 0;
49  }
50 
52  operands.empty() || operands.size() == 1,
53  "array constructor must have at most one operand");
54 
55  if(operands.empty() && cpp_is_pod(object_tc.type()))
56  return {};
57 
58  const exprt &size_expr = to_array_type(object_tc.type()).size();
59 
60  if(size_expr.id() == ID_infinity)
61  return {}; // don't initialize
62 
63  exprt tmp_size=size_expr;
64  make_constant_index(tmp_size);
65 
66  mp_integer s;
67  if(to_integer(to_constant_expr(tmp_size), s))
68  {
69  error().source_location=source_location;
70  error() << "array size '" << to_string(size_expr) << "' is not a constant"
71  << eom;
72  throw 0;
73  }
74 
75  /*if(cpp_is_pod(object_tc.type()))
76  {
77  code_expressiont new_code;
78  exprt op_tc=operands.front();
79  typecheck_expr(op_tc);
80  // Override constantness
81  object_tc.type().set("ID_C_constant", false);
82  object_tc.set("ID_C_lvalue", true);
83  side_effect_exprt assign(ID_assign);
84  assign.add_source_location()=source_location;
85  assign.copy_to_operands(object_tc, op_tc);
86  typecheck_side_effect_assignment(assign);
87  new_code.expression()=assign;
88  return new_code;
89  }
90  else*/
91  {
92  code_blockt new_code;
93 
94  // for each element of the array, call the default constructor
95  for(mp_integer i=0; i < s; ++i)
96  {
97  exprt::operandst tmp_operands;
98 
99  exprt constant = from_integer(i, c_index_type());
100  constant.add_source_location()=source_location;
101 
102  index_exprt index = index_exprt(object_tc, constant);
103  index.add_source_location()=source_location;
104 
105  if(!operands.empty())
106  {
107  index_exprt operand(operands.front(), constant);
108  operand.add_source_location()=source_location;
109  tmp_operands.push_back(operand);
110  }
111 
112  auto i_code = cpp_constructor(source_location, index, tmp_operands);
113 
114  if(i_code.has_value())
115  new_code.add(std::move(i_code.value()));
116  }
117  return std::move(new_code);
118  }
119  }
120  else if(cpp_is_pod(object_tc.type()))
121  {
122  exprt::operandst operands_tc=operands;
123 
124  for(auto &op : operands_tc)
125  {
126  typecheck_expr(op);
128  }
129 
130  if(operands_tc.empty())
131  {
132  // a POD is NOT initialized
133  return {};
134  }
135  else if(operands_tc.size()==1)
136  {
137  // Override constantness
138  object_tc.type().set(ID_C_constant, false);
139  object_tc.set(ID_C_lvalue, true);
141  object_tc, operands_tc.front(), typet(), source_location);
143  return code_expressiont(std::move(assign));
144  }
145  else
146  {
147  error().source_location=source_location;
148  error() << "initialization of POD requires one argument, "
149  "but got " << operands.size() << eom;
150  throw 0;
151  }
152  }
153  else if(object_tc.type().id() == ID_union_tag)
154  {
155  UNREACHABLE; // Todo: union
156  }
157  else if(object_tc.type().id() == ID_struct_tag)
158  {
159  exprt::operandst operands_tc=operands;
160 
161  for(auto &op : operands_tc)
162  {
163  typecheck_expr(op);
165  }
166 
167  const struct_typet &struct_type =
168  follow_tag(to_struct_tag_type(object_tc.type()));
169 
170  // set most-derived bits
171  code_blockt block;
172  for(const auto &component : struct_type.components())
173  {
174  if(component.get_base_name() != "@most_derived")
175  continue;
176 
177  member_exprt member(object_tc, component.get_name(), bool_typet());
178  member.add_source_location()=source_location;
179  member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue));
180 
181  exprt val=false_exprt();
182 
183  if(!component.get_bool(ID_from_base))
184  val=true_exprt();
185 
187  std::move(member), std::move(val), typet(), source_location);
188 
190 
191  block.add(code_expressiont(std::move(assign)));
192  }
193 
194  // enter struct scope
195  cpp_save_scopet save_scope(cpp_scopes);
196  cpp_scopes.set_scope(struct_type.get(ID_name));
197 
198  // find name of constructor
199  const struct_typet::componentst &components=
200  struct_type.components();
201 
202  irep_idt constructor_name;
203 
204  for(const auto &c : components)
205  {
206  const typet &type = c.type();
207 
208  if(
209  !c.get_bool(ID_from_base) && type.id() == ID_code &&
210  to_code_type(type).return_type().id() == ID_constructor)
211  {
212  constructor_name = c.get_base_name();
213  break;
214  }
215  }
216 
217  INVARIANT(!constructor_name.empty(), "non-PODs should have a constructor");
218 
219  side_effect_expr_function_callt function_call(
220  cpp_namet(constructor_name, source_location).as_expr(),
221  operands_tc,
223  source_location);
224 
226  CHECK_RETURN(function_call.get(ID_statement) == ID_temporary_object);
227 
228  exprt &initializer =
229  static_cast<exprt &>(function_call.add(ID_initializer));
230 
232  initializer.id() == ID_code &&
233  initializer.get(ID_statement) == ID_expression,
234  "initializer must be expression statement");
235 
236  auto &statement_expr = to_code_expression(to_code(initializer));
237 
239  to_side_effect_expr_function_call(statement_expr.expression());
240 
241  exprt &tmp_this=func_ini.arguments().front();
243  to_address_of_expr(tmp_this).object().id() == ID_new_object,
244  "expected new_object operand in address_of expression");
245 
246  tmp_this=address_of_exprt(object_tc);
247 
248  const auto &initializer_code=to_code(initializer);
249 
250  if(block.statements().empty())
251  return initializer_code;
252  else
253  {
254  block.add(initializer_code);
255  return std::move(block);
256  }
257  }
258  else
259  UNREACHABLE;
260 
261  return {};
262 }
263 
265  const source_locationt &source_location,
266  const typet &type,
267  const exprt::operandst &ops,
268  exprt &temporary)
269 {
270  // create temporary object
271  side_effect_exprt tmp_object_expr(ID_temporary_object, type, source_location);
272  tmp_object_expr.set(ID_mode, ID_cpp);
273 
274  exprt new_object(ID_new_object);
275  new_object.add_source_location()=tmp_object_expr.source_location();
276  new_object.set(ID_C_lvalue, true);
277  new_object.type()=tmp_object_expr.type();
278 
280 
281  auto new_code = cpp_constructor(source_location, new_object, ops);
282 
283  if(new_code.has_value())
284  {
285  if(new_code->get_statement() == ID_assign)
286  tmp_object_expr.add_to_operands(std::move(new_code->op1()));
287  else
288  tmp_object_expr.add(ID_initializer) = *new_code;
289  }
290 
291  temporary.swap(tmp_object_expr);
292 }
293 
295  const source_locationt &source_location,
296  const typet &type,
297  const exprt &op,
298  exprt &temporary)
299 {
300  exprt::operandst ops;
301  ops.push_back(op);
302  new_temporary(source_location, type, ops, temporary);
303 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
bitvector_typet c_index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: pointer_expr.h:540
static void make_already_typechecked(exprt &expr)
const exprt & size() const
Definition: std_types.h:840
The Boolean type.
Definition: std_types.h:36
virtual void make_constant_index(exprt &expr)
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
code_operandst & statements()
Definition: std_code.h:138
codet representation of an expression statement.
Definition: std_code.h:1394
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:87
void typecheck_side_effect_assignment(side_effect_exprt &) override
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
std::optional< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
void elaborate_class_template(const typet &type)
elaborate class template instances
void add_implicit_dereference(exprt &)
void typecheck_expr(exprt &) override
std::string to_string(const typet &) override
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:92
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
The Boolean constant false.
Definition: std_expr.h:3082
Array index operator.
Definition: std_expr.h:1470
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
irept & add(const irep_idt &name)
Definition: irep.cpp:103
Extract member of struct or union.
Definition: std_expr.h:2854
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
static eomt eom
Definition: message.h:289
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A side_effect_exprt that performs an assignment.
Definition: std_code.h:1565
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1692
exprt::operandst & arguments()
Definition: std_code.h:1718
An expression containing a side effect.
Definition: std_code.h:1450
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
The Boolean constant true.
Definition: std_expr.h:3073
The type of an expression, extends irept.
Definition: type.h:29
C++ Language Type Checking.
API to expression classes for Pointers.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:145
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1428
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:97
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518