CBMC
dfcc_is_freeable.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 Date: August 2022
7 
8 \*******************************************************************/
9 #include "dfcc_is_freeable.h"
10 
11 #include <util/cprover_prefix.h>
12 #include <util/std_expr.h>
13 #include <util/symbol.h>
14 
15 #include "dfcc_cfg_info.h"
16 #include "dfcc_library.h"
17 
19  dfcc_libraryt &library,
20  message_handlert &message_handler)
21  : library(library), message_handler(message_handler)
22 {
23 }
24 
26  goto_programt &program,
27  dfcc_cfg_infot &cfg_info)
28 {
30  program,
31  program.instructions.begin(),
32  program.instructions.end(),
33  cfg_info);
34 }
35 
37  goto_programt &program,
38  goto_programt::targett first_instruction,
39  const goto_programt::targett &last_instruction,
40  dfcc_cfg_infot &cfg_info)
41 {
42  auto target = first_instruction;
43  while(target != last_instruction)
44  {
45  if(target->is_function_call())
46  {
47  const auto &function = target->call_function();
48 
49  if(function.id() == ID_symbol)
50  {
51  const irep_idt &fun_name = to_symbol_expr(function).get_identifier();
52 
53  if(fun_name == CPROVER_PREFIX "is_freeable")
54  {
55  // redirect call to library implementation
56  to_symbol_expr(target->call_function())
58  target->call_arguments().push_back(cfg_info.get_write_set(target));
59  }
60  else if(fun_name == CPROVER_PREFIX "was_freed")
61  {
62  // insert call to precondition for vacuity checking
65  target->call_arguments().at(0),
66  cfg_info.get_write_set(target),
67  target->source_location()),
68  target->source_location());
69  program.insert_before_swap(target, inst);
70  target++;
71 
72  // redirect call to library implementation
73  to_symbol_expr(target->call_function())
75  target->call_arguments().push_back(cfg_info.get_write_set(target));
76  }
77  }
78  }
79  target++;
80  }
81 }
Computes natural loops, enforces normal form conditions, computes the nesting graph,...
const exprt & get_write_set(goto_programt::const_targett target) const
Returns the write set variable to use for the given instruction Returns the write set for the loop,...
void rewrite_calls(goto_programt &program, dfcc_cfg_infot &cfg_info)
Rewrites calls to is_freeable and was_freed predicates into calls to the library implementation in th...
dfcc_is_freeablet(dfcc_libraryt &library, message_handlert &message_handler)
dfcc_libraryt & library
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
const irep_idt & get_dfcc_fun_name(dfcc_funt fun) const
Returns the name of the given dfcc_funt.
const code_function_callt check_replace_ensures_was_freed_preconditions_call(const exprt &ptr, const exprt &write_set_ptr, const source_locationt &source_location)
Builds call to __CPROVER_contracts_check_replace_ensures_was_freed_preconditions.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
const source_locationt & source_location() const
Definition: expr.h:231
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
instructionst::iterator targett
Definition: goto_program.h:614
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:155
const irep_idt & get_identifier() const
Definition: std_expr.h:160
#define CPROVER_PREFIX
Class that computes CFG information about the loop structure of a GOTO function for the purpose of dy...
Instruments occurrences of is_freeable predicates in programs encoding requires and ensures clauses o...
Dynamic frame condition checking library loading.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
Symbol table entry.