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(to_constant_expr(tmp_size), s))
72  {
73  error().source_location=source_location;
74  error() << "array size '" << to_string(size_expr) << "' is not a constant"
75  << 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);
145  object_tc, operands_tc.front(), typet(), source_location);
147  return code_expressiont(std::move(assign));
148  }
149  else
150  {
151  error().source_location=source_location;
152  error() << "initialization of POD requires one argument, "
153  "but got " << operands.size() << eom;
154  throw 0;
155  }
156  }
157  else if(tmp_type.id()==ID_union)
158  {
159  UNREACHABLE; // Todo: union
160  }
161  else if(tmp_type.id()==ID_struct)
162  {
163  exprt::operandst operands_tc=operands;
164 
165  for(auto &op : operands_tc)
166  {
167  typecheck_expr(op);
169  }
170 
171  const struct_typet &struct_type=
172  to_struct_type(tmp_type);
173 
174  // set most-derived bits
175  code_blockt block;
176  for(const auto &component : struct_type.components())
177  {
178  if(component.get_base_name() != "@most_derived")
179  continue;
180 
181  member_exprt member(object_tc, component.get_name(), bool_typet());
182  member.add_source_location()=source_location;
183  member.set(ID_C_lvalue, object_tc.get_bool(ID_C_lvalue));
184 
185  exprt val=false_exprt();
186 
187  if(!component.get_bool(ID_from_base))
188  val=true_exprt();
189 
191  std::move(member), std::move(val), typet(), source_location);
192 
194 
195  block.add(code_expressiont(std::move(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  INVARIANT(!constructor_name.empty(), "non-PODs should have a constructor");
222 
223  side_effect_expr_function_callt function_call(
224  cpp_namet(constructor_name, source_location).as_expr(),
225  operands_tc,
227  source_location);
228 
230  assert(function_call.get(ID_statement)==ID_temporary_object);
231 
232  exprt &initializer =
233  static_cast<exprt &>(function_call.add(ID_initializer));
234 
235  assert(initializer.id()==ID_code &&
236  initializer.get(ID_statement)==ID_expression);
237 
238  auto &statement_expr = to_code_expression(to_code(initializer));
239 
241  to_side_effect_expr_function_call(statement_expr.expression());
242 
243  exprt &tmp_this=func_ini.arguments().front();
245  to_address_of_expr(tmp_this).object().id() == ID_new_object,
246  "expected new_object operand in address_of expression");
247 
248  tmp_this=address_of_exprt(object_tc);
249 
250  const auto &initializer_code=to_code(initializer);
251 
252  if(block.statements().empty())
253  return initializer_code;
254  else
255  {
256  block.add(initializer_code);
257  return std::move(block);
258  }
259  }
260  else
261  UNREACHABLE;
262 
263  return {};
264 }
265 
267  const source_locationt &source_location,
268  const typet &type,
269  const exprt::operandst &ops,
270  exprt &temporary)
271 {
272  // create temporary object
273  side_effect_exprt tmp_object_expr(ID_temporary_object, type, source_location);
274  tmp_object_expr.set(ID_mode, ID_cpp);
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 
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.add_to_operands(std::move(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 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
to_code_expression
code_expressiont & to_code_expression(codet &code)
Definition: std_code.h:1844
to_side_effect_expr_function_call
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:2182
cpp_typecheckt::elaborate_class_template
void elaborate_class_template(const typet &type)
elaborate class template instances
Definition: cpp_instantiate_template.cpp:224
arith_tools.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
cpp_save_scopet
Definition: cpp_scopes.h:129
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
typet
The type of an expression, extends irept.
Definition: type.h:29
cpp_typecheckt::typecheck_side_effect_assignment
void typecheck_side_effect_assignment(side_effect_exprt &) override
Definition: cpp_typecheck_expr.cpp:1997
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2117
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
cpp_typecheckt::new_temporary
void new_temporary(const source_locationt &source_location, const typet &, const exprt::operandst &ops, exprt &temporary)
Definition: cpp_constructor.cpp:266
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
cpp_typecheckt::cpp_constructor
optionalt< codet > cpp_constructor(const source_locationt &source_location, const exprt &object, const exprt::operandst &operands)
Definition: cpp_constructor.cpp:25
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
to_integer
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:19
bool_typet
The Boolean type.
Definition: std_types.h:37
messaget::eom
static eomt eom
Definition: message.h:297
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
array_typet::size
const exprt & size() const
Definition: std_types.h:973
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
cpp_typecheckt::cpp_is_pod
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
messaget::error
mstreamt & error() const
Definition: message.h:399
cpp_typecheckt::typecheck_side_effect_function_call
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
Definition: cpp_typecheck_expr.cpp:1494
already_typechecked_exprt::make_already_typechecked
static void make_already_typechecked(exprt &expr)
Definition: c_typecheck_base.h:289
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
cpp_util.h
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:2823
cpp_typecheckt::add_implicit_dereference
void add_implicit_dereference(exprt &)
Definition: cpp_typecheck_expr.cpp:1481
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
std_types.h
Pre-defined types.
side_effect_expr_assignt
A side_effect_exprt that performs an assignment.
Definition: std_code.h:1990
irept::swap
void swap(irept &irep)
Definition: irep.h:463
c_typecheck_baset::make_constant_index
virtual void make_constant_index(exprt &expr)
Definition: c_typecheck_expr.cpp:3573
irept::id
const irep_idt & id() const
Definition: irep.h:418
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
cpp_typecheck.h
C++ Language Type Checking.
source_locationt
Definition: source_location.h:20
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2251
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
is_reference
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:133
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:2161
c_typecheck_baset::return_type
typet return_type
Definition: c_typecheck_base.h:157
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:157
cpp_typecheckt::to_string
std::string to_string(const typet &) override
Definition: cpp_typecheck.cpp:84
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
uninitialized_typet
Definition: cpp_parse_tree.h:32
cpp_namet
Definition: cpp_name.h:17
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h
cpp_scopest::set_scope
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
validation_modet::INVARIANT
@ INVARIANT
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939