cprover
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
27{
28 return found;
29}
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 {
62 const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
63 if(function_set.find(fun_name) == function_set.end())
64 {
65 function_set.insert(fun_name);
66 auto called_fun = goto_functions.function_map.find(fun_name);
67 if(called_fun == goto_functions.function_map.end())
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
95{
96 function_set.clear();
97}
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{
122 find_is_fresh_calls_visitort requires_visitor;
123 requires_visitor(requires);
124 for(auto it : requires_visitor.is_fresh_calls())
125 {
127 }
128}
129
131{
132 find_is_fresh_calls_visitort ensures_visitor;
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
146void is_fresh_baset::add_declarations(const std::string &decl_string)
147{
148 log.debug() << "Creating declarations: \n" << decl_string << "\n";
149
150 std::istringstream iss(decl_string);
151
152 ansi_c_languaget ansi_c_language;
156 ansi_c_language.parse(iss, "");
158
159 symbol_tablet tmp_symbol_table;
160 ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
161 exprt value = nil_exprt();
162
163 goto_functionst tmp_functions;
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 {
179 this->parent.get_symbol_table().insert(symbol_pair.second);
180 }
181 // Parameters are stored as scoped names in the symbol table.
182 else if(
183 (has_prefix(
184 id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") ||
186 id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) &&
187 parent.get_symbol_table().add(symbol_pair.second))
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
213 if(add_address_of)
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
228 code_contractst &_parent,
229 messaget _log,
230 irep_idt _fun_id)
231 : is_fresh_baset(_parent, _log, _fun_id)
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
275{
277}
278
280{
281 update_fn_call(ins, ensures_fn_name, false);
282}
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
296 code_contractst &_parent,
297 messaget _log,
298 irep_idt _fun_id)
299 : is_fresh_baset(_parent, _log, _fun_id)
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
342{
343 update_fn_call(ins, requires_fn_name, false);
344}
345
347{
349}
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.
Definition: pointer_expr.h:361
bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool parse(std::istream &instream, const std::string &path) override
goto_functionst & get_goto_functions()
Definition: contracts.cpp:958
symbol_tablet & get_symbol_table()
Definition: contracts.cpp:953
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.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:592
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
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
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
std::size_t next_unused_suffix(const std::string &prefix, std::size_t start_number) const
Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
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.
Definition: symbol_table.h:14
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
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
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
preprocessort preprocessor
Definition: config.h:233