CBMC
dfcc_swap_and_wrap.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 
7 \*******************************************************************/
8 
15 
16 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
17 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_SWAP_AND_WRAP_H
18 
19 #include <util/arith_tools.h>
20 #include <util/c_types.h>
21 #include <util/message.h>
22 #include <util/std_expr.h>
23 #include <util/std_types.h>
24 
26 
27 #include "dfcc_contract_handler.h"
28 #include "dfcc_instrument.h"
29 #include "dfcc_library.h"
30 #include "dfcc_spec_functions.h"
31 
32 #include <map>
33 #include <set>
34 
35 class goto_modelt;
36 class messaget;
37 class message_handlert;
38 class symbolt;
40 
42 {
43 public:
51 
53  const loop_contract_configt &loop_contract_config,
54  const irep_idt &function_id,
55  const irep_idt &contract_id,
56  std::set<irep_idt> &function_pointer_contracts,
57  bool allow_recursive_calls)
58  {
61  loop_contract_config,
62  function_id,
63  contract_id,
64  function_pointer_contracts,
65  allow_recursive_calls);
66  }
67 
69  const irep_idt &function_id,
70  const irep_idt &contract_id,
71  std::set<irep_idt> &function_pointer_contracts)
72  {
75  loop_contract_configt{false},
76  function_id,
77  contract_id,
78  function_pointer_contracts,
79  false);
80  }
81 
83  void get_swapped_functions(std::set<irep_idt> &dest) const;
84 
85 protected:
94 
96  static std::map<
97  irep_idt,
98  std::pair<irep_idt, std::pair<dfcc_contract_modet, loop_contract_configt>>>
100 
101  void swap_and_wrap(
102  const dfcc_contract_modet contract_mode,
103  const loop_contract_configt &loop_contract_config,
104  const irep_idt &function_id,
105  const irep_idt &contract_id,
106  std::set<irep_idt> &function_pointer_contracts,
107  bool allow_recursive_calls);
108 
111  void check_contract(
112  const loop_contract_configt &loop_contract_config,
113  const irep_idt &function_id,
114  const irep_idt &contract_id,
115  std::set<irep_idt> &function_pointer_contracts,
116  bool allow_recursive_calls);
117 
121  const irep_idt &function_id,
122  const irep_idt &contract_id,
123  std::set<irep_idt> &function_pointer_contracts);
124 };
125 #endif
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition: c_expr.h:233
A contract is represented by a function declaration or definition with contract clauses attached to i...
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
This class rewrites GOTO functions that use the built-ins:
goto_modelt & goto_model
void check_contract(const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
Swaps-and-wraps the given function_id in a wrapper function that checks the given contract_id.
message_handlert & message_handler
dfcc_spec_functionst & spec_functions
void swap_and_wrap_check(const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
dfcc_libraryt & library
dfcc_swap_and_wrapt(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_spec_functionst &spec_functions, dfcc_contract_handlert &contract_handler)
void swap_and_wrap_replace(const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts)
void get_swapped_functions(std::set< irep_idt > &dest) const
Adds the set of swapped functions to dest.
static std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, loop_contract_configt > > > cache
remember all functions that were swapped/wrapped and in which mode
dfcc_instrumentt & instrument
dfcc_contract_handlert & contract_handler
void replace_with_contract(const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts)
Swaps-and-wraps the given function_id in a wrapper function that models the abstract behaviour of con...
void swap_and_wrap(const dfcc_contract_modet contract_mode, const loop_contract_configt &loop_contract_config, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Symbol table entry.
Definition: symbol.h:28
Specialisation of dfcc_contract_handlert for contracts.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Goto Programs with Functions.
API to expression classes.
Pre-defined types.
Loop contract configurations.
dstringt irep_idt