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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1260
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
is_fresh_baset::add_declarations
void add_declarations(const std::string &decl_string)
Definition: memory_predicates.cpp:144
is_fresh_baset::requires_fn_name
std::string requires_fn_name
Definition: memory_predicates.h:51
is_fresh_baset::ensures_fn_name
std::string ensures_fn_name
Definition: memory_predicates.h:52
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
is_fresh_replacet::is_fresh_replacet
is_fresh_replacet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
Definition: memory_predicates.cpp:296
is_fresh_replacet::create_ensures_fn_call
virtual void create_ensures_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:347
is_fresh_enforcet::create_requires_fn_call
virtual void create_requires_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:275
configt::ansi_ct::preprocessort
preprocessort
Definition: config.h:197
prefix.h
functions_in_scope_visitort::function_calls
std::set< irep_idt > & function_calls()
Definition: memory_predicates.cpp:37
functions_in_scope_visitort::operator()
void operator()(const goto_programt &prog)
Definition: memory_predicates.cpp:42
exprt
Base class for all expressions.
Definition: expr.h:54
find_is_fresh_calls_visitort::operator()
void operator()(goto_programt &prog)
Definition: memory_predicates.cpp:97
irep_idt
dstringt irep_idt
Definition: irep.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
messaget::eom
static eomt eom
Definition: message.h:297
configt::ansi_c
struct configt::ansi_ct ansi_c
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1082
is_fresh_baset::update_ensures
void update_ensures(goto_programt &ensures)
Definition: memory_predicates.cpp:128
is_fresh_baset::parent
code_contractst & parent
Definition: memory_predicates.h:45
is_fresh_baset::log
messaget log
Definition: memory_predicates.h:46
memory_predicates.h
Predicates to specify memory footprint in function contracts.
is_fresh_replacet::create_requires_fn_call
virtual void create_requires_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:342
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:706
functions_in_scope_visitort::function_set
std::set< irep_idt > function_set
Definition: memory_predicates.h:144
as_const
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
messaget::error
mstreamt & error() const
Definition: message.h:399
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
configt::ansi_ct::preprocessor
preprocessort preprocessor
Definition: config.h:199
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
is_fresh_baset::update_fn_call
void update_fn_call(goto_programt::targett &target, const std::string &name, bool add_address_of)
Definition: memory_predicates.cpp:208
expr2c.h
is_fresh_enforcet::create_ensures_fn_call
virtual void create_ensures_fn_call(goto_programt::targett &target)
Definition: memory_predicates.cpp:280
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
nil_exprt
The NIL expression.
Definition: std_expr.h:2820
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1402
find_is_fresh_calls_visitort::function_set
std::set< goto_programt::targett > function_set
Definition: memory_predicates.h:101
is_fresh_baset::fun_id
irep_idt fun_id
Definition: memory_predicates.h:47
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
code_contractst
Definition: contracts.h:62
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:17
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
irept::id
const irep_idt & id() const
Definition: irep.h:407
functions_in_scope_visitort::log
messaget & log
Definition: memory_predicates.h:143
is_fresh_baset::create_ensures_fn_call
virtual void create_ensures_fn_call(goto_programt::targett &target)=0
config
configt config
Definition: config.cpp:25
return_value_visitort::operator()
void operator()(const exprt &exp) override
Definition: memory_predicates.cpp:29
is_fresh_baset
Definition: memory_predicates.h:20
find_is_fresh_calls_visitort
Predicate to be used with the exprt::visit() function.
Definition: memory_predicates.h:88
goto_programt::get_end_function
targett get_end_function()
Get an instruction iterator pointing to the END_FUNCTION instruction of the goto program.
Definition: goto_program.h:854
configt::ansi_ct::preprocessort::NONE
@ NONE
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
find_is_fresh_calls_visitort::is_fresh_calls
std::set< goto_programt::targett > & is_fresh_calls()
Definition: memory_predicates.cpp:87
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
array_typet
Arrays with given size.
Definition: std_types.h:763
ansi_c_language.h
is_fresh_enforcet::is_fresh_enforcet
is_fresh_enforcet(code_contractst &_parent, messaget _log, const irep_idt _fun_id)
Definition: memory_predicates.cpp:228
ansi_c_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: ansi_c_language.cpp:50
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
is_fresh_baset::memmap_name
std::string memmap_name
Definition: memory_predicates.h:50
code_contractst::get_symbol_table
symbol_tablet & get_symbol_table()
Definition: contracts.cpp:659
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
is_fresh_baset::create_requires_fn_call
virtual void create_requires_fn_call(goto_programt::targett &target)=0
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
config.h
is_fresh_enforcet::create_declarations
virtual void create_declarations()
Definition: memory_predicates.cpp:245
messaget::debug
mstreamt & debug() const
Definition: message.h:429
ansi_c_languaget::typecheck
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
Definition: ansi_c_language.cpp:103
static_lifetime_init.h
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
is_fresh_replacet::create_declarations
virtual void create_declarations()
Definition: memory_predicates.cpp:315
unique_symbol
std::string unique_symbol(const symbol_tablet &tbl, const std::string &original)
Definition: memory_predicates.cpp:290
return_value_visitort::found_return_value
bool found_return_value()
Definition: memory_predicates.cpp:24
code_contractst::get_goto_functions
goto_functionst & get_goto_functions()
Definition: contracts.cpp:664
symbol_table_baset::next_unused_suffix
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.
Definition: symbol_table_base.h:63
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
return_value_visitort::found
bool found
Definition: memory_predicates.h:120
messaget::warning
mstreamt & warning() const
Definition: message.h:404
goto_programt::instructiont
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
find_is_fresh_calls_visitort::clear_set
void clear_set()
Definition: memory_predicates.cpp:92
ansi_c_languaget
Definition: ansi_c_language.h:35
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:646
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1255
is_fresh_baset::update_requires
void update_requires(goto_programt &requires)
Definition: memory_predicates.cpp:118
functions_in_scope_visitort::goto_functions
const goto_functionst & goto_functions
Definition: memory_predicates.h:142