cprover
memory_predicates.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Predicates to specify memory footprint in function contracts.
4 
5 Author: Felipe R. Monteiro
6 
7 Date: July 2021
8 
9 \*******************************************************************/
10 
13 
14 #include "memory_predicates.h"
15 
16 #include <ansi-c/ansi_c_language.h>
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: "
57  << messaget::eom;
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 
89 std::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 
146 void 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;
153  ansi_c_language.set_message_handler(log.get_message_handler());
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) + "::") ||
185  has_prefix(
186  id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) &&
187  parent.get_symbol_table().add(symbol_pair.second))
188  {
189  UNREACHABLE;
190  }
191  }
192 
194  {
198  goto_convert(
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 {
276  update_fn_call(ins, requires_fn_name, true);
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 
289 std::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 {
348  update_fn_call(ins, ensures_fn_name, true);
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 & warning() const
Definition: message.h:404
mstreamt & debug() const
Definition: message.h:429
message_handlert & get_message_handler()
Definition: message.h:184
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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