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
17#include <ansi-c/expr2c.h>
18
20
22
23#include <util/config.h>
24#include <util/prefix.h>
25
30
32{
33 if(exp.id() != ID_symbol)
34 return;
35 const symbol_exprt &sym = to_symbol_expr(exp);
36 found |= sym.get_identifier() == CPROVER_PREFIX "return_value";
37}
38
40{
41 return function_set;
42}
43
45{
47 {
48 if(ins->is_function_call())
49 {
50 const auto &function = ins->call_function();
51
52 if(function.id() != ID_symbol)
53 {
54 log.error().source_location = ins->source_location();
55 log.error() << "Function pointer used in function invoked by "
56 "function contract: "
58 throw 0;
59 }
60 else
61 {
63 if(function_set.find(fun_name) == function_set.end())
64 {
65 function_set.insert(fun_name);
68 {
69 log.warning() << "Could not find function '" << fun_name
70 << "' in goto-program." << messaget::eom;
71 throw 0;
72 }
73 if(called_fun->second.body_available())
74 {
75 const goto_programt &program = called_fun->second.body;
76 (*this)(program);
77 }
78 else
79 {
80 log.warning() << "No body for function: " << fun_name
81 << "invoked from function contract." << messaget::eom;
82 }
83 }
84 }
85 }
86 }
87}
88
89std::set<goto_programt::targett> &find_is_fresh_calls_visitort::is_fresh_calls()
90{
91 return function_set;
92}
93
98
100{
102 {
103 if(ins->is_function_call())
104 {
105 const auto &function = ins->call_function();
106
107 if(function.id() == ID_symbol)
108 {
109 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
110
111 if(fun_name == (CPROVER_PREFIX + std::string("is_fresh")))
112 {
113 function_set.insert(ins);
114 }
115 }
116 }
117 }
118}
119
121{
123 requires_visitor(requires);
124 for(auto it : requires_visitor.is_fresh_calls())
125 {
127 }
128}
129
131{
133 ensures_visitor(ensures);
134 for(auto it : ensures_visitor.is_fresh_calls())
135 {
137 }
138}
139
140//
141//
142// Code largely copied from model_argc_argv.cpp
143//
144//
145
147{
148 log.debug() << "Creating declarations: \n" << decl_string << "\n";
149
150 std::istringstream iss(decl_string);
151
153 ansi_c_language.set_message_handler(log.get_message_handler());
156 ansi_c_language.parse(iss, "");
157 config.ansi_c.preprocessor = pp;
158
160 ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
161 exprt value = nil_exprt();
162
164
165 // Add the new functions into the goto functions table.
167 tmp_functions.function_map[ensures_fn_name]);
168
170 tmp_functions.function_map[requires_fn_name]);
171
172 for(const auto &symbol_pair : tmp_symbol_table.symbols)
173 {
174 if(
175 symbol_pair.first == memmap_name ||
176 symbol_pair.first == ensures_fn_name ||
177 symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc")
178 {
180 }
181 // Parameters are stored as scoped names in the symbol table.
182 else if(
183 (has_prefix(
188 {
190 }
191 }
192
194 {
204 }
205}
206
209 const std::string &fn_name,
210 bool add_address_of)
211{
212 // adjusting the expression for the first argument, if required
214 {
215 INVARIANT(
216 as_const(*ins).call_arguments().size() > 0,
217 "Function must have arguments");
218 ins->call_arguments()[0] = address_of_exprt(ins->call_arguments()[0]);
219 }
220
221 // fixing the function name.
222 to_symbol_expr(ins->call_function()).set_identifier(fn_name);
223}
224
225/* Declarations for contract enforcement */
226
232{
233 std::stringstream ssreq, ssensure, ssmemmap;
234 ssreq << CPROVER_PREFIX << fun_id << "_requires_is_fresh";
235 this->requires_fn_name = ssreq.str();
236
237 ssensure << CPROVER_PREFIX << fun_id << "_ensures_is_fresh";
238 this->ensures_fn_name = ssensure.str();
239
240 ssmemmap << CPROVER_PREFIX << fun_id << "_memory_map";
241 this->memmap_name = ssmemmap.str();
242}
243
245{
246 std::ostringstream oss;
247 std::string cprover_prefix(CPROVER_PREFIX);
248 oss << "static _Bool " << memmap_name
249 << "[" + cprover_prefix + "constant_infinity_uint]; \n"
250 << "\n"
251 << "_Bool " << requires_fn_name
252 << "(void **elem, " + cprover_prefix + "size_t size) { \n"
253 << " *elem = malloc(size); \n"
254 << " if (!*elem || " << memmap_name
255 << "[" + cprover_prefix + "POINTER_OBJECT(*elem)]) return 0; \n"
256 << " " << memmap_name << "[" + cprover_prefix
257 << "POINTER_OBJECT(*elem)] = 1; \n"
258 << " return 1; \n"
259 << "} \n"
260 << "\n"
261 << "_Bool " << ensures_fn_name
262 << "(void *elem, " + cprover_prefix + "size_t size) { \n"
263 << " _Bool ok = (!" << memmap_name
264 << "[" + cprover_prefix + "POINTER_OBJECT(elem)] && "
265 << cprover_prefix + "r_ok(elem, size)); \n"
266 << " " << memmap_name << "[" + cprover_prefix
267 << "POINTER_OBJECT(elem)] = 1; \n"
268 << " return ok; \n"
269 << "}";
270
271 add_declarations(oss.str());
272}
273
278
283
284/* Declarations for contract replacement: note that there may be several
285 instances of the same function called in a particular context, so care must be taken
286 that the 'call' functions and global data structure are unique for each instance.
287 This is why we check that the symbols are unique for each such declaration. */
288
289std::string unique_symbol(const symbol_tablet &tbl, const std::string &original)
290{
291 auto size = tbl.next_unused_suffix(original);
292 return original + std::to_string(size);
293}
294
300{
301 std::stringstream ssreq, ssensure, ssmemmap;
302 ssreq /* << CPROVER_PREFIX */ << fun_id << "_call_requires_is_fresh";
303 this->requires_fn_name =
304 unique_symbol(parent.get_symbol_table(), ssreq.str());
305
306 ssensure /* << CPROVER_PREFIX */ << fun_id << "_call_ensures_is_fresh";
307 this->ensures_fn_name =
308 unique_symbol(parent.get_symbol_table(), ssensure.str());
309
310 ssmemmap /* << CPROVER_PREFIX */ << fun_id << "_memory_map";
311 this->memmap_name = unique_symbol(parent.get_symbol_table(), ssmemmap.str());
312}
313
315{
316 std::ostringstream oss;
317 std::string cprover_prefix(CPROVER_PREFIX);
318 oss << "static _Bool " << memmap_name
319 << "[" + cprover_prefix + "constant_infinity_uint]; \n"
320 << "\n"
321 << "static _Bool " << requires_fn_name
322 << "(void *elem, " + cprover_prefix + "size_t size) { \n"
323 << " _Bool r_ok = " + cprover_prefix + "r_ok(elem, size); \n"
324 << " if (" << memmap_name
325 << "[" + cprover_prefix + "POINTER_OBJECT(elem)]"
326 << " != 0 || !r_ok) return 0; \n"
327 << " " << memmap_name << "["
328 << cprover_prefix + "POINTER_OBJECT(elem)] = 1; \n"
329 << " return 1; \n"
330 << "} \n"
331 << " \n"
332 << "_Bool " << ensures_fn_name
333 << "(void **elem, " + cprover_prefix + "size_t size) { \n"
334 << " *elem = malloc(size); \n"
335 << " return (*elem != 0); \n"
336 << "} \n";
337
338 add_declarations(oss.str());
339}
340
345
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
goto_functionst & get_goto_functions()
symbol_tablet & get_symbol_table()
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:37
Base class for all expressions.
Definition expr.h:54
Predicate to be used with the exprt::visit() function.
void operator()(goto_programt &prog)
std::set< goto_programt::targett > function_set
std::set< goto_programt::targett > & is_fresh_calls()
void operator()(const goto_programt &prog)
const goto_functionst & goto_functions
std::set< irep_idt > & function_calls()
std::set< irep_idt > function_set
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
const irep_idt & id() const
Definition irep.h:396
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
std::string ensures_fn_name
std::string requires_fn_name
code_contractst & parent
void update_requires(goto_programt &requires)
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
virtual void create_ensures_fn_call(goto_programt::targett &target)
virtual void create_requires_fn_call(goto_programt::targett &target)
is_fresh_enforcet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
virtual void create_declarations()
is_fresh_replacet(code_contractst &_parent, messaget _log, 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:247
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
The NIL expression.
Definition std_expr.h:2874
void operator()(const exprt &exp) override
Expression to hold a symbol (variable)
Definition std_expr.h:80
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:104
const irep_idt & get_identifier() const
Definition std_expr.h:109
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.
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
configt config
Definition config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
std::string unique_symbol(const symbol_tablet &tbl, const std::string &original)
Predicates to specify memory footprint in function contracts.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189