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 
21 #include <util/config.h>
22 #include <util/prefix.h>
23 
25 {
26  return found;
27 }
28 
30 {
31  if(exp.id() != ID_symbol)
32  return;
33  const symbol_exprt &sym = to_symbol_expr(exp);
34  found |= sym.get_identifier() == CPROVER_PREFIX "return_value";
35 }
36 
38 {
39  return function_set;
40 }
41 
43 {
45  {
46  if(ins->is_function_call())
47  {
48  const auto &function = ins->call_function();
49 
50  if(function.id() != ID_symbol)
51  {
52  log.error().source_location = ins->source_location;
53  log.error() << "Function pointer used in function invoked by "
54  "function contract: "
55  << messaget::eom;
56  throw 0;
57  }
58  else
59  {
60  const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
61  if(function_set.find(fun_name) == function_set.end())
62  {
63  function_set.insert(fun_name);
64  auto called_fun = goto_functions.function_map.find(fun_name);
65  if(called_fun == goto_functions.function_map.end())
66  {
67  log.warning() << "Could not find function '" << fun_name
68  << "' in goto-program." << messaget::eom;
69  throw 0;
70  }
71  if(called_fun->second.body_available())
72  {
73  const goto_programt &program = called_fun->second.body;
74  (*this)(program);
75  }
76  else
77  {
78  log.warning() << "No body for function: " << fun_name
79  << "invoked from function contract." << messaget::eom;
80  }
81  }
82  }
83  }
84  }
85 }
86 
87 std::set<goto_programt::targett> &find_is_fresh_calls_visitort::is_fresh_calls()
88 {
89  return function_set;
90 }
91 
93 {
94  function_set.clear();
95 }
96 
98 {
100  {
101  if(ins->is_function_call())
102  {
103  const auto &function = ins->call_function();
104 
105  if(function.id() == ID_symbol)
106  {
107  const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
108 
109  if(fun_name == (CPROVER_PREFIX + std::string("is_fresh")))
110  {
111  function_set.insert(ins);
112  }
113  }
114  }
115  }
116 }
117 
119 {
120  find_is_fresh_calls_visitort requires_visitor;
121  requires_visitor(requires);
122  for(auto it : requires_visitor.is_fresh_calls())
123  {
125  }
126 }
127 
129 {
130  find_is_fresh_calls_visitort ensures_visitor;
131  ensures_visitor(ensures);
132  for(auto it : ensures_visitor.is_fresh_calls())
133  {
135  }
136 }
137 
138 //
139 //
140 // Code largely copied from model_argc_argv.cpp
141 //
142 //
143 
144 void is_fresh_baset::add_declarations(const std::string &decl_string)
145 {
146  log.debug() << "Creating declarations: \n" << decl_string << "\n";
147 
148  std::istringstream iss(decl_string);
149 
150  ansi_c_languaget ansi_c_language;
151  ansi_c_language.set_message_handler(log.get_message_handler());
154  ansi_c_language.parse(iss, "");
156 
157  symbol_tablet tmp_symbol_table;
158  ansi_c_language.typecheck(tmp_symbol_table, "<built-in-library>");
159  exprt value = nil_exprt();
160 
161  goto_functionst tmp_functions;
162 
163  // Add the new functions into the goto functions table.
165  tmp_functions.function_map[ensures_fn_name]);
166 
168  tmp_functions.function_map[requires_fn_name]);
169 
170  for(const auto &symbol_pair : tmp_symbol_table.symbols)
171  {
172  if(
173  symbol_pair.first == memmap_name ||
174  symbol_pair.first == ensures_fn_name ||
175  symbol_pair.first == requires_fn_name || symbol_pair.first == "malloc")
176  {
177  this->parent.get_symbol_table().insert(symbol_pair.second);
178  }
179  // Parameters are stored as scoped names in the symbol table.
180  else if(
181  (has_prefix(
182  id2string(symbol_pair.first), id2string(ensures_fn_name) + "::") ||
183  has_prefix(
184  id2string(symbol_pair.first), id2string(requires_fn_name) + "::")) &&
185  parent.get_symbol_table().add(symbol_pair.second))
186  {
187  UNREACHABLE;
188  }
189  }
190 
191  // We have to set the global memory map array to
192  // all zeros for this to work properly
193  const array_typet ty =
194  to_array_type(tmp_symbol_table.lookup_ref(memmap_name).type);
195  constant_exprt initial_value(irep_idt(dstringt("0")), ty.subtype());
196  array_of_exprt memmap_init(initial_value, ty);
199 
200  // insert the assignment into the initialize function.
201  auto called_func =
203  goto_programt &body = called_func->second.body;
204  auto target = body.get_end_function();
205  body.insert_before(target, a);
206 }
207 
210  const std::string &fn_name,
211  bool add_address_of)
212 {
213  // adjusting the expression for the first argument, if required
214  if(add_address_of)
215  {
216  INVARIANT(
217  as_const(*ins).call_arguments().size() > 0,
218  "Function must have arguments");
219  ins->call_arguments()[0] = address_of_exprt(ins->call_arguments()[0]);
220  }
221 
222  // fixing the function name.
223  to_symbol_expr(ins->call_function()).set_identifier(fn_name);
224 }
225 
226 /* Declarations for contract enforcement */
227 
229  code_contractst &_parent,
230  messaget _log,
231  irep_idt _fun_id)
232  : is_fresh_baset(_parent, _log, _fun_id)
233 {
234  std::stringstream ssreq, ssensure, ssmemmap;
235  ssreq << CPROVER_PREFIX << fun_id << "_requires_is_fresh";
236  this->requires_fn_name = ssreq.str();
237 
238  ssensure << CPROVER_PREFIX << fun_id << "_ensures_is_fresh";
239  this->ensures_fn_name = ssensure.str();
240 
241  ssmemmap << CPROVER_PREFIX << fun_id << "_memory_map";
242  this->memmap_name = ssmemmap.str();
243 }
244 
246 {
247  std::ostringstream oss;
248  std::string cprover_prefix(CPROVER_PREFIX);
249  oss << "static _Bool " << memmap_name
250  << "[" + cprover_prefix + "constant_infinity_uint]; \n"
251  << "\n"
252  << "_Bool " << requires_fn_name
253  << "(void **elem, " + cprover_prefix + "size_t size) { \n"
254  << " *elem = malloc(size); \n"
255  << " if (!*elem || " << memmap_name
256  << "[" + cprover_prefix + "POINTER_OBJECT(*elem)]) return 0; \n"
257  << " " << memmap_name << "[" + cprover_prefix
258  << "POINTER_OBJECT(*elem)] = 1; \n"
259  << " return 1; \n"
260  << "} \n"
261  << "\n"
262  << "_Bool " << ensures_fn_name
263  << "(void *elem, " + cprover_prefix + "size_t size) { \n"
264  << " _Bool ok = (!" << memmap_name
265  << "[" + cprover_prefix + "POINTER_OBJECT(elem)] && "
266  << cprover_prefix + "r_ok(elem, size)); \n"
267  << " " << memmap_name << "[" + cprover_prefix
268  << "POINTER_OBJECT(elem)] = 1; \n"
269  << " return ok; \n"
270  << "}";
271 
272  add_declarations(oss.str());
273 }
274 
276 {
277  update_fn_call(ins, requires_fn_name, true);
278 }
279 
281 {
282  update_fn_call(ins, ensures_fn_name, false);
283 }
284 
285 /* Declarations for contract replacement: note that there may be several
286  instances of the same function called in a particular context, so care must be taken
287  that the 'call' functions and global data structure are unique for each instance.
288  This is why we check that the symbols are unique for each such declaration. */
289 
290 std::string unique_symbol(const symbol_tablet &tbl, const std::string &original)
291 {
292  auto size = tbl.next_unused_suffix(original);
293  return original + std::to_string(size);
294 }
295 
297  code_contractst &_parent,
298  messaget _log,
299  irep_idt _fun_id)
300  : is_fresh_baset(_parent, _log, _fun_id)
301 {
302  std::stringstream ssreq, ssensure, ssmemmap;
303  ssreq /* << CPROVER_PREFIX */ << fun_id << "_call_requires_is_fresh";
304  this->requires_fn_name =
305  unique_symbol(parent.get_symbol_table(), ssreq.str());
306 
307  ssensure /* << CPROVER_PREFIX */ << fun_id << "_call_ensures_is_fresh";
308  this->ensures_fn_name =
309  unique_symbol(parent.get_symbol_table(), ssensure.str());
310 
311  ssmemmap /* << CPROVER_PREFIX */ << fun_id << "_memory_map";
312  this->memmap_name = unique_symbol(parent.get_symbol_table(), ssmemmap.str());
313 }
314 
316 {
317  std::ostringstream oss;
318  std::string cprover_prefix(CPROVER_PREFIX);
319  oss << "static _Bool " << memmap_name
320  << "[" + cprover_prefix + "constant_infinity_uint]; \n"
321  << "\n"
322  << "static _Bool " << requires_fn_name
323  << "(void *elem, " + cprover_prefix + "size_t size) { \n"
324  << " _Bool r_ok = " + cprover_prefix + "r_ok(elem, size); \n"
325  << " if (" << memmap_name
326  << "[" + cprover_prefix + "POINTER_OBJECT(elem)]"
327  << " != 0 || !r_ok) return 0; \n"
328  << " " << memmap_name << "["
329  << cprover_prefix + "POINTER_OBJECT(elem)] = 1; \n"
330  << " return 1; \n"
331  << "} \n"
332  << " \n"
333  << "_Bool " << ensures_fn_name
334  << "(void **elem, " + cprover_prefix + "size_t size) { \n"
335  << " *elem = malloc(size); \n"
336  << " return (*elem != 0); \n"
337  << "} \n";
338 
339  add_declarations(oss.str());
340 }
341 
343 {
344  update_fn_call(ins, requires_fn_name, false);
345 }
346 
348 {
349  update_fn_call(ins, ensures_fn_name, true);
350 }
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:341
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
Array constructor from single element.
Definition: std_expr.h:1402
Arrays with given size.
Definition: std_types.h:763
goto_functionst & get_goto_functions()
Definition: contracts.cpp:664
symbol_tablet & get_symbol_table()
Definition: contracts.cpp:659
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2753
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
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst::iterator targett
Definition: goto_program.h:646
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:854
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:706
const irep_idt & id() const
Definition: irep.h:407
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:2820
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.
typet type
Type of symbol.
Definition: symbol.h:31
const typet & subtype() const
Definition: type.h:47
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
dstringt irep_idt
Definition: irep.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
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 INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
preprocessort preprocessor
Definition: config.h:199