cprover
Loading...
Searching...
No Matches
memory_predicates.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Predicates to specify memory footprint in function contracts.
4
5Author: Felipe R. Monteiro
6
7Date: July 2021
8
9\*******************************************************************/
10
13
14#include "memory_predicates.h"
15
16#include <util/arith_tools.h>
17#include <util/c_types.h>
18#include <util/config.h>
19#include <util/fresh_symbol.h>
20#include <util/prefix.h>
21
25
27#include "utils.h"
28
30{
31 return function_set;
32}
33
35{
37
39 {
40 if(ins->is_function_call())
41 {
42 const auto &function = ins->call_function();
43
44 if(function.id() != ID_symbol)
45 {
46 log.error().source_location = ins->source_location();
47 log.error() << "Function pointer used in function invoked by "
48 "function contract: "
50 throw 0;
51 }
52 else
53 {
54 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
55 if(function_set.find(fun_name) == function_set.end())
56 {
57 function_set.insert(fun_name);
58 auto called_fun = goto_functions.function_map.find(fun_name);
59 if(called_fun == goto_functions.function_map.end())
60 {
61 log.warning() << "Could not find function '" << fun_name
62 << "' in goto-program." << messaget::eom;
63 throw 0;
64 }
65 if(called_fun->second.body_available())
66 {
67 const goto_programt &program = called_fun->second.body;
68 (*this)(program);
69 }
70 else
71 {
72 log.warning() << "No body for function: " << fun_name
73 << "invoked from function contract." << messaget::eom;
74 }
75 }
76 }
77 }
78 }
79}
80
81std::set<goto_programt::targett, goto_programt::target_less_than> &
86
91
93{
95 {
96 if(ins->is_function_call())
97 {
98 const auto &function = ins->call_function();
99
100 if(function.id() == ID_symbol)
101 {
102 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
103
104 if(fun_name == (CPROVER_PREFIX + std::string("is_fresh")))
105 {
106 function_set.insert(ins);
107 }
108 }
109 }
110 }
111}
112
114{
115 find_is_fresh_calls_visitort requires_visitor;
116 requires_visitor(requires_);
117 for(auto it : requires_visitor.is_fresh_calls())
118 {
120 }
121}
122
124{
125 find_is_fresh_calls_visitort ensures_visitor;
126 ensures_visitor(ensures);
127 for(auto it : ensures_visitor.is_fresh_calls())
128 {
130 }
131}
132
133//
134//
135// Code largely copied from model_argc_argv.cpp
136//
137//
138
143
145{
146 source_locationt source_location;
147 add_pragma_disable_assigns_check(source_location);
148 auto memmap_type = get_memmap_type();
149 program.add(
150 goto_programt::make_decl(memmap_symbol.symbol_expr(), source_location));
152 memmap_symbol.symbol_expr(),
154 from_integer(0, get_memmap_type().element_type()), get_memmap_type()),
155 source_location));
156}
157
159{
160 source_locationt source_location;
161 add_pragma_disable_assigns_check(source_location);
162 program.add(
163 goto_programt::make_dead(memmap_symbol.symbol_expr(), source_location));
164}
165
166void is_fresh_baset::add_declarations(const std::string &decl_string)
167{
169 log.debug() << "Creating declarations: \n" << decl_string << "\n";
170
171 std::istringstream iss(decl_string);
172
173 ansi_c_languaget ansi_c_language;
174 configt::ansi_ct::preprocessort pp = config.ansi_c.preprocessor;
175 config.ansi_c.preprocessor = configt::ansi_ct::preprocessort::NONE;
176 ansi_c_language.parse(iss, "", log.get_message_handler());
177 config.ansi_c.preprocessor = pp;
178
179 symbol_tablet tmp_symbol_table;
180 ansi_c_language.typecheck(
181 tmp_symbol_table, "<built-in-library>", log.get_message_handler());
182 exprt value = nil_exprt();
183
184 goto_functionst tmp_functions;
185
186 // Add the new functions into the goto functions table.
187 goto_model.goto_functions.function_map[ensures_fn_name].copy_from(
188 tmp_functions.function_map[ensures_fn_name]);
189
190 goto_model.goto_functions.function_map[requires_fn_name].copy_from(
191 tmp_functions.function_map[requires_fn_name]);
192
193 for(const auto &symbol_pair : tmp_symbol_table.symbols)
194 {
195 if(
196 symbol_pair.first == memmap_name ||
197 symbol_pair.first == ensures_fn_name ||
198 symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc")
199 {
200 goto_model.symbol_table.insert(symbol_pair.second);
201 }
202 // Parameters are stored as scoped names in the symbol table.
203 else if(
204 (has_prefix(
205 id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") ||
207 id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) &&
208 goto_model.symbol_table.add(symbol_pair.second))
209 {
211 }
212 }
213
214 if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
216}
217
220 const std::string &fn_name,
221 bool add_address_of)
222{
223 // adjusting the expression for the first argument, if required
224 if(add_address_of)
225 {
226 INVARIANT(
227 as_const(*ins).call_arguments().size() > 0,
228 "Function must have arguments");
229 ins->call_arguments()[0] = address_of_exprt(ins->call_arguments()[0]);
230 }
231
232 // fixing the function name.
233 to_symbol_expr(ins->call_function()).set_identifier(fn_name);
234
235 // pass the memory mmap
236 ins->call_arguments().push_back(address_of_exprt(
237 index_exprt(memmap_symbol.symbol_expr(), from_integer(0, c_index_type()))));
238}
239
240/* Declarations for contract enforcement */
241
245 const irep_idt &_fun_id)
247{
248 std::stringstream ssreq, ssensure, ssmemmap;
249 ssreq << CPROVER_PREFIX "enforce_requires_is_fresh";
250 this->requires_fn_name = ssreq.str();
251
252 ssensure << CPROVER_PREFIX "enforce_ensures_is_fresh";
253 this->ensures_fn_name = ssensure.str();
254
255 ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id;
256 this->memmap_name = ssmemmap.str();
257
258 const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode;
261 "",
262 this->memmap_name,
264 mode,
265 goto_model.symbol_table);
266}
267
269{
270 // Check if symbols are already declared
271 if(goto_model.symbol_table.has_symbol(requires_fn_name))
272 return;
273
274 std::ostringstream oss;
275 std::string cprover_prefix(CPROVER_PREFIX);
276 oss << "_Bool " << requires_fn_name
277 << "(void **elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
278 << "#pragma CPROVER check push\n"
279 << "#pragma CPROVER check disable \"pointer\"\n"
280 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
281 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
282 << "#pragma CPROVER check disable \"signed-overflow\"\n"
283 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
284 << "#pragma CPROVER check disable \"conversion\"\n"
285 << " *elem = malloc(size); \n"
286 << " if (!*elem) return 0; \n"
287 << " mmap[" + cprover_prefix + "POINTER_OBJECT(*elem)] = 1; \n"
288 << " return 1; \n"
289 << "#pragma CPROVER check pop\n"
290 << "} \n"
291 << "\n"
292 << "_Bool " << ensures_fn_name
293 << "(void *elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
294 << "#pragma CPROVER check push\n"
295 << "#pragma CPROVER check disable \"pointer\"\n"
296 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
297 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
298 << "#pragma CPROVER check disable \"signed-overflow\"\n"
299 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
300 << "#pragma CPROVER check disable \"conversion\"\n"
301 << " _Bool ok = (!mmap[" + cprover_prefix + "POINTER_OBJECT(elem)] && "
302 << cprover_prefix + "r_ok(elem, size)); \n"
303 << " mmap[" + cprover_prefix << "POINTER_OBJECT(elem)] = 1; \n"
304 << " return ok; \n"
305 << "#pragma CPROVER check pop\n"
306 << "}";
307
308 add_declarations(oss.str());
309}
310
315
320
324 const irep_idt &_fun_id)
326{
327 std::stringstream ssreq, ssensure, ssmemmap;
328 ssreq << CPROVER_PREFIX "replace_requires_is_fresh";
329 this->requires_fn_name = ssreq.str();
330
331 ssensure << CPROVER_PREFIX "replace_ensures_is_fresh";
332 this->ensures_fn_name = ssensure.str();
333
334 ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id;
335 this->memmap_name = ssmemmap.str();
336
337 const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode;
340 "",
341 this->memmap_name,
343 mode,
344 goto_model.symbol_table);
345}
346
348{
349 // Check if symbols are already declared
350 if(goto_model.symbol_table.has_symbol(requires_fn_name))
351 return;
352
353 std::ostringstream oss;
354 std::string cprover_prefix(CPROVER_PREFIX);
355 oss << "static _Bool " << requires_fn_name
356 << "(void *elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
357 << "#pragma CPROVER check push\n"
358 << "#pragma CPROVER check disable \"pointer\"\n"
359 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
360 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
361 << "#pragma CPROVER check disable \"signed-overflow\"\n"
362 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
363 << "#pragma CPROVER check disable \"conversion\"\n"
364 << " _Bool r_ok = " + cprover_prefix + "r_ok(elem, size); \n"
365 << " if (mmap[" + cprover_prefix + "POINTER_OBJECT(elem)]"
366 << " != 0 || !r_ok) return 0; \n"
367 << " mmap[" << cprover_prefix + "POINTER_OBJECT(elem)] = 1; \n"
368 << " return 1; \n"
369 << "#pragma CPROVER check pop\n"
370 << "} \n"
371 << " \n"
372 << "_Bool " << ensures_fn_name
373 << "(void **elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
374 << "#pragma CPROVER check push\n"
375 << "#pragma CPROVER check disable \"pointer\"\n"
376 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
377 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
378 << "#pragma CPROVER check disable \"signed-overflow\"\n"
379 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
380 << "#pragma CPROVER check disable \"conversion\"\n"
381 << " *elem = malloc(size); \n"
382 << " return (*elem != 0); \n"
383 << "#pragma CPROVER check pop\n"
384 << "} \n";
385
386 add_declarations(oss.str());
387}
388
393
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
unsignedbv_typet size_type()
Definition c_types.cpp:50
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:127
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
Array constructor from single element.
Definition std_expr.h:1558
Arrays with given size.
Definition std_types.h:807
Base class for all expressions.
Definition expr.h:56
Predicate to be used with the exprt::visit() function.
void operator()(goto_programt &prog)
std::set< goto_programt::targett, goto_programt::target_less_than > & is_fresh_calls()
std::set< goto_programt::targett, goto_programt::target_less_than > function_set
void operator()(const goto_programt &prog)
const goto_functionst & goto_functions
std::set< irep_idt > & function_calls()
std::set< irep_idt > function_set
message_handlert & message_handler
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Array index operator.
Definition std_expr.h:1470
An expression denoting infinity.
Definition std_expr.h:3229
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
const irep_idt & fun_id
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
std::string ensures_fn_name
message_handlert & message_handler
std::string requires_fn_name
void add_memory_map_decl(goto_programt &program)
void update_requires(goto_programt &requires_)
void add_memory_map_dead(goto_programt &program)
array_typet get_memmap_type()
goto_modelt & goto_model
void add_declarations(const std::string &decl_string)
std::string memmap_name
is_fresh_baset(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
void update_ensures(goto_programt &ensures)
virtual void create_requires_fn_call(goto_programt::targett &target)=0
is_fresh_enforcet(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_requires_fn_call(goto_programt::targett &target)
virtual void create_declarations()
is_fresh_replacet(goto_modelt &goto_model, message_handlert &message_handler, const irep_idt &_fun_id)
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_declarations()
virtual void create_requires_fn_call(goto_programt::targett &target)
source_locationt source_location
Definition message.h:239
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
mstreamt & debug() const
Definition message.h:421
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & warning() const
Definition message.h:396
static eomt eom
Definition message.h:289
The NIL expression.
Definition std_expr.h:3213
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:155
const irep_idt & get_identifier() const
Definition std_expr.h:160
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
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.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
void add_pragma_disable_assigns_check(source_locationt &location)
Adds a pragma on a source_locationt to disable inclusion checking.
Specify write set in function contracts.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Predicates to specify memory footprint in function contracts.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
dstringt irep_idt