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  {
42  case lifetimet::AUTOMATIC_LOCAL:
44  assignments, target_expr, allocate_type, basename_prefix);
45  break;
46 
47  case lifetimet::STATIC_GLOBAL:
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 }
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:1788
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:28
fresh_symbol.h
Fresh auxiliary symbol creation.
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:386
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:219
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:54
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:80
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:82
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: pointer_expr.h:461
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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:125
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
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:92
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:33
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
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:33
irept::id
const irep_idt & id() const
Definition: irep.h:407
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
allocate_objectst::name_prefix
const irep_idt name_prefix
Definition: allocate_objects.h:106
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:227
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:181
code_inputt
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:677
symbolt
Symbol table entry.
Definition: symbol.h:28
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:256
size_of_expr
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:278
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:172
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:245
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:330
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:243
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:71
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:238
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:1898