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
23
26
28#include "utils.h"
29
31{
32 return function_set;
33}
34
36{
38
40 {
41 if(ins->is_function_call())
42 {
43 const auto &function = ins->call_function();
44
45 if(function.id() != ID_symbol)
46 {
47 log.error().source_location = ins->source_location();
48 log.error() << "Function pointer used in function invoked by "
49 "function contract: "
51 throw 0;
52 }
53 else
54 {
55 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
56 if(function_set.find(fun_name) == function_set.end())
57 {
58 function_set.insert(fun_name);
59 auto called_fun = goto_functions.function_map.find(fun_name);
60 if(called_fun == goto_functions.function_map.end())
61 {
62 log.warning() << "Could not find function '" << fun_name
63 << "' in goto-program." << messaget::eom;
64 throw 0;
65 }
66 if(called_fun->second.body_available())
67 {
68 const goto_programt &program = called_fun->second.body;
69 (*this)(program);
70 }
71 else
72 {
73 log.warning() << "No body for function: " << fun_name
74 << "invoked from function contract." << messaget::eom;
75 }
76 }
77 }
78 }
79 }
80}
81
82std::set<goto_programt::targett, goto_programt::target_less_than> &
87
92
94{
96 {
97 if(ins->is_function_call())
98 {
99 const auto &function = ins->call_function();
100
101 if(function.id() == ID_symbol)
102 {
103 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
104
105 if(fun_name == (CPROVER_PREFIX + std::string("is_fresh")))
106 {
107 function_set.insert(ins);
108 }
109 }
110 }
111 }
112}
113
123
133
134//
135//
136// Code largely copied from model_argc_argv.cpp
137//
138//
139
144
146{
147 source_locationt source_location;
148 add_pragma_disable_assigns_check(source_location);
150 program.add(
155 from_integer(0, get_memmap_type().element_type()), get_memmap_type()),
156 source_location));
157}
158
160{
161 source_locationt source_location;
162 add_pragma_disable_assigns_check(source_location);
163 program.add(
165}
166
168{
170 log.debug() << "Creating declarations: \n" << decl_string << "\n";
171
172 std::istringstream iss(decl_string);
173
175 ansi_c_language.set_message_handler(message_handler);
178 ansi_c_language.parse(iss, "");
179 config.ansi_c.preprocessor = pp;
180
182 ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
183 exprt value = nil_exprt();
184
186
187 // Add the new functions into the goto functions table.
189 tmp_functions.function_map[ensures_fn_name]);
190
192 tmp_functions.function_map[requires_fn_name]);
193
194 for(const auto &symbol_pair : tmp_symbol_table.symbols)
195 {
196 if(
197 symbol_pair.first == memmap_name ||
198 symbol_pair.first == ensures_fn_name ||
199 symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc")
200 {
202 }
203 // Parameters are stored as scoped names in the symbol table.
204 else if(
205 (has_prefix(
210 {
212 }
213 }
214
217}
218
221 const std::string &fn_name,
222 bool add_address_of)
223{
224 // adjusting the expression for the first argument, if required
226 {
227 INVARIANT(
228 as_const(*ins).call_arguments().size() > 0,
229 "Function must have arguments");
230 ins->call_arguments()[0] = address_of_exprt(ins->call_arguments()[0]);
231 }
232
233 // fixing the function name.
234 to_symbol_expr(ins->call_function()).set_identifier(fn_name);
235
236 // pass the memory mmap
237 ins->call_arguments().push_back(address_of_exprt(
239}
240
241/* Declarations for contract enforcement */
242
244 goto_modelt &goto_model,
245 message_handlert &message_handler,
246 const irep_idt &_fun_id)
247 : is_fresh_baset(goto_model, message_handler, _fun_id)
248{
249 std::stringstream ssreq, ssensure, ssmemmap;
250 ssreq << CPROVER_PREFIX "enforce_requires_is_fresh";
251 this->requires_fn_name = ssreq.str();
252
253 ssensure << CPROVER_PREFIX "enforce_ensures_is_fresh";
254 this->ensures_fn_name = ssensure.str();
255
256 ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id;
257 this->memmap_name = ssmemmap.str();
258
259 const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode;
262 "",
263 this->memmap_name,
265 mode,
267}
268
270{
271 // Check if symbols are already declared
273 return;
274
275 std::ostringstream oss;
276 std::string cprover_prefix(CPROVER_PREFIX);
277 oss << "_Bool " << requires_fn_name
278 << "(void **elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
279 << "#pragma CPROVER check push\n"
280 << "#pragma CPROVER check disable \"pointer\"\n"
281 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
282 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
283 << "#pragma CPROVER check disable \"signed-overflow\"\n"
284 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
285 << "#pragma CPROVER check disable \"conversion\"\n"
286 << " *elem = malloc(size); \n"
287 << " if (!*elem) return 0; \n"
288 << " mmap[" + cprover_prefix + "POINTER_OBJECT(*elem)] = 1; \n"
289 << " return 1; \n"
290 << "#pragma CPROVER check pop\n"
291 << "} \n"
292 << "\n"
293 << "_Bool " << ensures_fn_name
294 << "(void *elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
295 << "#pragma CPROVER check push\n"
296 << "#pragma CPROVER check disable \"pointer\"\n"
297 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
298 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
299 << "#pragma CPROVER check disable \"signed-overflow\"\n"
300 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
301 << "#pragma CPROVER check disable \"conversion\"\n"
302 << " _Bool ok = (!mmap[" + cprover_prefix + "POINTER_OBJECT(elem)] && "
303 << cprover_prefix + "r_ok(elem, size)); \n"
304 << " mmap[" + cprover_prefix << "POINTER_OBJECT(elem)] = 1; \n"
305 << " return ok; \n"
306 << "#pragma CPROVER check pop\n"
307 << "}";
308
309 add_declarations(oss.str());
310}
311
316
321
323 goto_modelt &goto_model,
324 message_handlert &message_handler,
325 const irep_idt &_fun_id)
326 : is_fresh_baset(goto_model, message_handler, _fun_id)
327{
328 std::stringstream ssreq, ssensure, ssmemmap;
329 ssreq << CPROVER_PREFIX "replace_requires_is_fresh";
330 this->requires_fn_name = ssreq.str();
331
332 ssensure << CPROVER_PREFIX "replace_ensures_is_fresh";
333 this->ensures_fn_name = ssensure.str();
334
335 ssmemmap << CPROVER_PREFIX "is_fresh_memory_map_" << fun_id;
336 this->memmap_name = ssmemmap.str();
337
338 const auto &mode = goto_model.symbol_table.lookup_ref(_fun_id).mode;
341 "",
342 this->memmap_name,
344 mode,
346}
347
349{
350 // Check if symbols are already declared
352 return;
353
354 std::ostringstream oss;
355 std::string cprover_prefix(CPROVER_PREFIX);
356 oss << "static _Bool " << requires_fn_name
357 << "(void *elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
358 << "#pragma CPROVER check push\n"
359 << "#pragma CPROVER check disable \"pointer\"\n"
360 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
361 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
362 << "#pragma CPROVER check disable \"signed-overflow\"\n"
363 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
364 << "#pragma CPROVER check disable \"conversion\"\n"
365 << " _Bool r_ok = " + cprover_prefix + "r_ok(elem, size); \n"
366 << " if (mmap[" + cprover_prefix + "POINTER_OBJECT(elem)]"
367 << " != 0 || !r_ok) return 0; \n"
368 << " mmap[" << cprover_prefix + "POINTER_OBJECT(elem)] = 1; \n"
369 << " return 1; \n"
370 << "#pragma CPROVER check pop\n"
371 << "} \n"
372 << " \n"
373 << "_Bool " << ensures_fn_name
374 << "(void **elem, " + cprover_prefix + "size_t size, _Bool *mmap) { \n"
375 << "#pragma CPROVER check push\n"
376 << "#pragma CPROVER check disable \"pointer\"\n"
377 << "#pragma CPROVER check disable \"pointer-primitive\"\n"
378 << "#pragma CPROVER check disable \"pointer-overflow\"\n"
379 << "#pragma CPROVER check disable \"signed-overflow\"\n"
380 << "#pragma CPROVER check disable \"unsigned-overflow\"\n"
381 << "#pragma CPROVER check disable \"conversion\"\n"
382 << " *elem = malloc(size); \n"
383 << " return (*elem != 0); \n"
384 << "#pragma CPROVER check pop\n"
385 << "} \n";
386
387 add_declarations(oss.str());
388}
389
394
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:55
unsignedbv_typet unsigned_char_type()
Definition c_types.cpp:132
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Array constructor from single element.
Definition std_expr.h:1498
Arrays with given size.
Definition std_types.h:763
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition goto_model.h:95
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
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:1410
An expression denoting infinity.
Definition std_expr.h:3042
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
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)
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
The NIL expression.
Definition std_expr.h:3026
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
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:47
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:222