CBMC
dfcc_lift_memory_predicates.h
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: November 2022
7 
8 \*******************************************************************/
9 
18 
19 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
20 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LIFT_MEMORY_PREDICATES_H
21 
22 #include <util/message.h>
23 
25 
26 #include <map>
27 #include <set>
28 
29 class dfcc_libraryt;
30 class dfcc_instrumentt;
31 class message_handlert;
32 class goto_modelt;
33 class exprt;
34 class replace_symbolt;
35 
37 {
38 public:
47  message_handlert &message_handler);
48 
53  std::set<irep_idt>
54  lift_predicates(std::set<irep_idt> &discovered_function_pointer_contracts);
55 
58  void fix_calls(goto_programt &program);
59 
63  void fix_calls(
64  goto_programt &program,
65  goto_programt::targett first_instruction,
66  const goto_programt::targett &last_instruction);
67 
68 protected:
73  // index of lifted parameters for lifted functions
74  std::map<irep_idt, std::set<std::size_t>> lifted_parameters;
75 
79  const goto_programt &goto_program,
80  const std::set<irep_idt> &predicates);
81 
82  void lift_predicate(
83  const irep_idt &function_id,
84  std::set<irep_idt> &discovered_function_pointer_contracts);
85 
87  const irep_idt &function_id,
88  std::set<irep_idt> &discovered_function_pointer_contracts);
89 
96  void add_pointer_type(
97  const irep_idt &function_id,
98  const std::size_t parameter_rank,
99  replace_symbolt &replace_lifted_param);
100 
103  void collect_parameters_to_lift(const irep_idt &function_id);
104 
106  bool is_lifted_function(const irep_idt &function_id);
107 };
108 
109 #endif
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
void fix_calls(goto_programt &program)
Fixes calls to user-defined memory predicates in the given program, by adding an address-of to argume...
void collect_parameters_to_lift(const irep_idt &function_id)
Computes the subset of function parameters of function_id that are passed directly to core predicates...
void lift_predicate(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
void add_pointer_type(const irep_idt &function_id, const std::size_t parameter_rank, replace_symbolt &replace_lifted_param)
adds a pointer_type to the parameter of a function
dfcc_lift_memory_predicatest(goto_modelt &goto_model, dfcc_libraryt &library, dfcc_instrumentt &instrument, message_handlert &message_handler)
std::map< irep_idt, std::set< std::size_t > > lifted_parameters
void lift_parameters_and_update_body(const irep_idt &function_id, std::set< irep_idt > &discovered_function_pointer_contracts)
bool calls_memory_predicates(const goto_programt &goto_program, const std::set< irep_idt > &predicates)
Returns true iff goto_program calls core memory predicates.
bool is_lifted_function(const irep_idt &function_id)
True if a function at least had one of its parameters lifted.
std::set< irep_idt > lift_predicates(std::set< irep_idt > &discovered_function_pointer_contracts)
Collects and lifts all user-defined memory predicates.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
Replace a symbol expression by a given expression.
Concrete Goto Program.