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 "arith_tools.h"
12 #include "c_types.h"
13 #include "fresh_symbol.h"
14 #include "pointer_expr.h"
15 #include "pointer_offset_size.h"
16 #include "string_constant.h"
17 
34  code_blockt &assignments,
35  const exprt &target_expr,
36  const typet &allocate_type,
37  const lifetimet lifetime,
38  const irep_idt &basename_prefix)
39 {
40  switch(lifetime)
41  {
44  assignments, target_expr, allocate_type, basename_prefix);
45  break;
46 
49  assignments, target_expr, allocate_type, basename_prefix);
50  break;
51 
52  case lifetimet::DYNAMIC:
53  return allocate_dynamic_object(assignments, target_expr, allocate_type);
54  break;
55  }
56 
58 }
59 
72  code_blockt &assignments,
73  const exprt &target_expr,
74  const typet &allocate_type,
75  const irep_idt &basename_prefix)
76 {
78  assignments, target_expr, allocate_type, false, basename_prefix);
79 }
80 
93  code_blockt &assignments,
94  const exprt &target_expr,
95  const typet &allocate_type,
96  const irep_idt &basename_prefix)
97 {
99  assignments, target_expr, allocate_type, true, basename_prefix);
100 }
101 
109  const typet &allocate_type,
110  const irep_idt &basename_prefix)
111 {
112  symbolt &aux_symbol = get_fresh_aux_symbol(
113  allocate_type,
115  id2string(basename_prefix),
117  symbol_mode,
118  symbol_table);
119 
120  symbols_created.push_back(&aux_symbol);
121 
122  return aux_symbol.symbol_expr();
123 }
124 
126  code_blockt &output_code,
127  const exprt &target_expr,
128  const typet &allocate_type)
129 {
130  if(allocate_type.id() == ID_empty)
131  {
132  // make null
133  code_assignt code{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  symbols_created.push_back(&malloc_sym);
157 
158  code_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_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  symbols_created.push_back(&aux_symbol);
198 
200  address_of_exprt(aux_symbol.symbol_expr()), target_expr.type());
201 
202  code_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_ptr);
222 }
223 
228 {
229  // Add the following code to init_code for each symbol that's been created:
230  // <type> <identifier>;
231  for(const symbolt *const symbol_ptr : symbols_created)
232  {
233  if(!symbol_ptr->is_static_lifetime)
234  {
235  code_declt decl(symbol_ptr->symbol_expr());
237  init_code.add(decl);
238  }
239  }
240 }
241 
246 {
247  // Add the following code to init_code for each symbol that's been created:
248  // INPUT("<identifier>", <identifier>);
249  for(symbolt const *symbol_ptr : symbols_created)
250  {
251  init_code.add(code_inputt{
252  symbol_ptr->base_name, symbol_ptr->symbol_expr(), source_location});
253  }
254 }
255 
257 {
258  side_effect_exprt alloc{
259  ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()};
260  return code_assignt(lhs, alloc);
261 }
code_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:243
Operator to return the address of an object.
Definition: pointer_expr.h:200
std::vector< const symbolt * > symbols_created
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
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...
void add_created_symbol(const symbolt *symbol_ptr)
Add a pointer to a symbol to the list of pointers to symbols created so far.
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 an assignment in the program.
Definition: std_code.h:295
A codet representing sequential composition of program statements.
Definition: std_code.h:170
void add(const codet &code)
Definition: std_code.h:208
A codet representing the declaration of a local variable.
Definition: std_code.h:402
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:677
Operator to dereference a pointer.
Definition: pointer_expr.h:256
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:239
const source_locationt & source_location() const
Definition: expr.h:234
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2726
const irep_idt & id() const
Definition: irep.h:407
The null pointer constant.
Definition: std_expr.h:2751
An expression containing a side effect.
Definition: std_code.h:1898
Expression to hold a symbol (variable)
Definition: std_expr.h:81
Symbol table entry.
Definition: symbol.h:28
bool is_static_lifetime
Definition: symbol.h:65
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
The type of an expression, extends irept.
Definition: type.h:28
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:49
API to expression classes for Pointers.
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:504
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1533