cprover
allocate_objects.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "allocate_objects.h"
10 
11 #include <util/c_types.h>
12 #include <util/fresh_symbol.h>
13 #include <util/pointer_expr.h>
15 #include <util/symbol.h>
16 
33  code_blockt &assignments,
34  const exprt &target_expr,
35  const typet &allocate_type,
36  const lifetimet lifetime,
37  const irep_idt &basename_prefix)
38 {
39  switch(lifetime)
40  {
43  assignments, target_expr, allocate_type, basename_prefix);
44  break;
45 
48  assignments, target_expr, allocate_type, basename_prefix);
49  break;
50 
51  case lifetimet::DYNAMIC:
52  return allocate_dynamic_object(assignments, target_expr, allocate_type);
53  break;
54  }
55 
57 }
58 
71  code_blockt &assignments,
72  const exprt &target_expr,
73  const typet &allocate_type,
74  const irep_idt &basename_prefix)
75 {
77  assignments, target_expr, allocate_type, false, basename_prefix);
78 }
79 
92  code_blockt &assignments,
93  const exprt &target_expr,
94  const typet &allocate_type,
95  const irep_idt &basename_prefix)
96 {
98  assignments, target_expr, allocate_type, true, basename_prefix);
99 }
100 
108  const typet &allocate_type,
109  const irep_idt &basename_prefix)
110 {
111  symbolt &aux_symbol = get_fresh_aux_symbol(
112  allocate_type,
114  id2string(basename_prefix),
116  symbol_mode,
117  symbol_table);
118 
119  add_created_symbol(aux_symbol);
120 
121  return aux_symbol.symbol_expr();
122 }
123 
125  code_blockt &output_code,
126  const exprt &target_expr,
127  const typet &allocate_type)
128 {
129  if(allocate_type.id() == ID_empty)
130  {
131  // make null
133  target_expr,
134  null_pointer_exprt{to_pointer_type(target_expr.type())},
136  output_code.add(std::move(code));
137 
138  return exprt();
139  }
140 
141  // build size expression
142  auto object_size = size_of_expr(allocate_type, ns);
143  INVARIANT(object_size.has_value(), "Size of objects should be known");
144 
145  // create a symbol for the malloc expression so we can initialize
146  // without having to do it potentially through a double-deref, which
147  // breaks the to-SSA phase.
148  symbolt &malloc_sym = get_fresh_aux_symbol(
149  pointer_type(allocate_type),
151  "malloc_site",
153  symbol_mode,
154  symbol_table);
155 
156  add_created_symbol(malloc_sym);
157 
158  code_frontend_assignt assign =
159  make_allocate_code(malloc_sym.symbol_expr(), object_size.value());
160  output_code.add(assign);
161 
162  exprt malloc_symbol_expr = typecast_exprt::conditional_cast(
163  malloc_sym.symbol_expr(), target_expr.type());
164 
165  code_frontend_assignt code(target_expr, malloc_symbol_expr);
167  output_code.add(code);
168 
169  return malloc_sym.symbol_expr();
170 }
171 
173  code_blockt &output_code,
174  const exprt &target_expr,
175  const typet &allocate_type)
176 {
177  return dereference_exprt(
178  allocate_dynamic_object_symbol(output_code, target_expr, allocate_type));
179 }
180 
182  code_blockt &assignments,
183  const exprt &target_expr,
184  const typet &allocate_type,
185  const bool static_lifetime,
186  const irep_idt &basename_prefix)
187 {
188  symbolt &aux_symbol = get_fresh_aux_symbol(
189  allocate_type,
191  id2string(basename_prefix),
193  symbol_mode,
194  symbol_table);
195 
196  aux_symbol.is_static_lifetime = static_lifetime;
197  add_created_symbol(aux_symbol);
198 
200  address_of_exprt(aux_symbol.symbol_expr()), target_expr.type());
201 
202  code_frontend_assignt code(target_expr, aoe);
204  assignments.add(code);
205 
206  if(aoe.id() == ID_typecast)
207  {
208  return dereference_exprt(aoe);
209  }
210  else
211  {
212  return aux_symbol.symbol_expr();
213  }
214 }
215 
220 {
221  symbols_created.push_back(symbol.name);
222 }
223 
228 {
229  // Add the following code to init_code for each symbol that's been created:
230  // <type> <identifier>;
231  for(const auto &symbol_id : symbols_created)
232  {
233  const symbolt &symbol = ns.lookup(symbol_id);
234  if(!symbol.is_static_lifetime)
235  {
236  code_declt decl{symbol.symbol_expr()};
238  init_code.add(decl);
239  }
240  }
241 }
242 
247 {
248  // Add the following code to init_code for each symbol that's been created:
249  // INPUT("<identifier>", <identifier>);
250  for(const auto &symbol_id : symbols_created)
251  {
252  const symbolt &symbol = ns.lookup(symbol_id);
253  init_code.add(
254  code_inputt{symbol.base_name, symbol.symbol_expr(), source_location});
255  }
256 }
257 
259 make_allocate_code(const symbol_exprt &lhs, const exprt &size)
260 {
261  side_effect_exprt alloc{
262  ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()};
263  return code_frontend_assignt(lhs, alloc);
264 }
code_frontend_assignt make_allocate_code(const symbol_exprt &lhs, const exprt &size)
Create code allocating an object of size size and assigning it to lhs
lifetimet
Selects the kind of objects allocated.
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
Operator to return the address of an object.
Definition: pointer_expr.h:361
void add_created_symbol(const symbolt &symbol)
Add a pointer to a symbol to the list of pointers to symbols created so far.
exprt allocate_non_dynamic_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const bool static_lifetime, const irep_idt &basename_prefix)
const namespacet ns
const irep_idt symbol_mode
std::vector< irep_idt > symbols_created
const irep_idt name_prefix
exprt allocate_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const lifetimet lifetime, const irep_idt &basename_prefix="tmp")
Allocates a new object, either by creating a local variable with automatic lifetime,...
symbol_table_baset & symbol_table
const source_locationt source_location
exprt allocate_dynamic_object_symbol(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generates code for allocating a dynamic object.
exprt allocate_dynamic_object(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generate the same code as allocate_dynamic_object_symbol, but return a dereference_exprt that derefer...
exprt allocate_static_global_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a global variable with static lifetime.
void mark_created_symbols_as_input(code_blockt &init_code)
Adds code to mark the created symbols as input.
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
A codet representing the declaration of a local variable.
A codet representing an assignment in the program.
Definition: std_code.h:24
A codet representing the declaration that an input of a particular description has a value which corr...
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
const irep_idt & id() const
Definition: irep.h:396
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The null pointer constant.
Definition: pointer_expr.h:723
An expression containing a side effect.
Definition: std_code.h:1450
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
irep_idt name
The unique identifier.
Definition: symbol.h:40
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Pointer Logic.
exprt object_size(const exprt &pointer)
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
Symbol table entry.