cprover
allocate_objects.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
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),
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,
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",
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),
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(
255 }
256}
257
259make_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
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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.