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_offset_size.h"
15 #include "string_constant.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  symbols_created.push_back(&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
132  code_assignt code{target_expr,
133  null_pointer_exprt{to_pointer_type(target_expr.type())},
135  output_code.add(std::move(code));
136 
137  return exprt();
138  }
139 
140  // build size expression
141  auto object_size = size_of_expr(allocate_type, ns);
142  INVARIANT(object_size.has_value(), "Size of objects should be known");
143 
144  // create a symbol for the malloc expression so we can initialize
145  // without having to do it potentially through a double-deref, which
146  // breaks the to-SSA phase.
147  symbolt &malloc_sym = get_fresh_aux_symbol(
148  pointer_type(allocate_type),
150  "malloc_site",
152  symbol_mode,
153  symbol_table);
154 
155  symbols_created.push_back(&malloc_sym);
156 
157  code_assignt assign =
158  make_allocate_code(malloc_sym.symbol_expr(), object_size.value());
159  output_code.add(assign);
160 
161  exprt malloc_symbol_expr = typecast_exprt::conditional_cast(
162  malloc_sym.symbol_expr(), target_expr.type());
163 
164  code_assignt code(target_expr, malloc_symbol_expr);
166  output_code.add(code);
167 
168  return malloc_sym.symbol_expr();
169 }
170 
172  code_blockt &output_code,
173  const exprt &target_expr,
174  const typet &allocate_type)
175 {
176  return dereference_exprt(
177  allocate_dynamic_object_symbol(output_code, target_expr, allocate_type));
178 }
179 
181  code_blockt &assignments,
182  const exprt &target_expr,
183  const typet &allocate_type,
184  const bool static_lifetime,
185  const irep_idt &basename_prefix)
186 {
187  symbolt &aux_symbol = get_fresh_aux_symbol(
188  allocate_type,
190  id2string(basename_prefix),
192  symbol_mode,
193  symbol_table);
194 
195  aux_symbol.is_static_lifetime = static_lifetime;
196  symbols_created.push_back(&aux_symbol);
197 
199  address_of_exprt(aux_symbol.symbol_expr()), target_expr.type());
200 
201  code_assignt code(target_expr, aoe);
203  assignments.add(code);
204 
205  if(aoe.id() == ID_typecast)
206  {
207  return dereference_exprt(aoe);
208  }
209  else
210  {
211  return aux_symbol.symbol_expr();
212  }
213 }
214 
219 {
220  symbols_created.push_back(symbol_ptr);
221 }
222 
227 {
228  // Add the following code to init_code for each symbol that's been created:
229  // <type> <identifier>;
230  for(const symbolt *const symbol_ptr : symbols_created)
231  {
232  if(!symbol_ptr->is_static_lifetime)
233  {
234  code_declt decl(symbol_ptr->symbol_expr());
236  init_code.add(decl);
237  }
238  }
239 }
240 
245 {
246  // Add the following code to init_code for each symbol that's been created:
247  // INPUT("<identifier>", <identifier>);
248  for(symbolt const *symbol_ptr : symbols_created)
249  {
250  init_code.add(code_inputt{
251  symbol_ptr->base_name, symbol_ptr->symbol_expr(), source_location});
252  }
253 }
254 
256 {
257  side_effect_exprt alloc{
258  ID_allocate, {size, false_exprt()}, lhs.type(), lhs.source_location()};
259  return code_assignt(lhs, alloc);
260 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
arith_tools.h
lifetimet::AUTOMATIC_LOCAL
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
typet
The type of an expression, extends irept.
Definition: type.h:29
fresh_symbol.h
Fresh auxiliary symbol creation.
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
allocate_objectst::add_created_symbol
void add_created_symbol(const symbolt *symbol_ptr)
Add a pointer to a symbol to the list of pointers to symbols created so far.
Definition: allocate_objects.cpp:218
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
allocate_objectst::symbol_table
symbol_table_baset & symbol_table
Definition: allocate_objects.h:108
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
allocate_objectst::symbol_mode
const irep_idt symbol_mode
Definition: allocate_objects.h:104
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
allocate_objectst::ns
const namespacet ns
Definition: allocate_objects.h:109
allocate_objectst::symbols_created
std::vector< const symbolt * > symbols_created
Definition: allocate_objects.h:111
null_pointer_exprt
The null pointer constant.
Definition: std_expr.h:3989
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
allocate_objectst::allocate_dynamic_object_symbol
exprt allocate_dynamic_object_symbol(code_blockt &output_code, const exprt &target_expr, const typet &allocate_type)
Generates code for allocating a dynamic object.
Definition: allocate_objects.cpp:124
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
allocate_objectst::allocate_static_global_object
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.
Definition: allocate_objects.cpp:91
allocate_objectst::allocate_object
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,...
Definition: allocate_objects.cpp:32
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
object_size
exprt object_size(const exprt &pointer)
Definition: pointer_predicates.cpp:32
irept::id
const irep_idt & id() const
Definition: irep.h:418
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
allocate_objectst::name_prefix
const irep_idt name_prefix
Definition: allocate_objects.h:106
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
allocate_objectst::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Definition: allocate_objects.cpp:226
lifetimet
lifetimet
Selects the kind of objects allocated.
Definition: allocate_objects.h:21
allocate_objectst::source_location
const source_locationt source_location
Definition: allocate_objects.h:105
allocate_objectst::allocate_non_dynamic_object
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)
Definition: allocate_objects.cpp:180
code_inputt
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:645
symbolt
Symbol table entry.
Definition: symbol.h:28
lifetimet::STATIC_GLOBAL
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
make_allocate_code
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
Definition: allocate_objects.cpp:255
lifetimet::DYNAMIC
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:285
allocate_objectst::allocate_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...
Definition: allocate_objects.cpp:171
allocate_objectst::mark_created_symbols_as_input
void mark_created_symbols_as_input(code_blockt &init_code)
Adds code to mark the created symbols as input.
Definition: allocate_objects.cpp:244
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
allocate_objectst::allocate_automatic_local_object
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.
Definition: allocate_objects.cpp:70
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
allocate_objects.h
c_types.h
get_fresh_aux_symbol
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 ...
Definition: fresh_symbol.cpp:32
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1866
validation_modet::INVARIANT
@ INVARIANT