cprover
Loading...
Searching...
No Matches
dfcc_swap_and_wrap.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking for function contracts
4
5Author: 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
28#include "dfcc_instrument.h"
29#include "dfcc_library.h"
30#include "dfcc_spec_functions.h"
31
32#include <map>
33#include <set>
34
35class goto_modelt;
36class messaget;
38class symbolt;
40
42{
43public:
51
53 const dfcc_loop_contract_modet loop_contract_mode,
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_mode,
62 function_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 {
76 function_id,
78 function_pointer_contracts,
79 false);
80 }
81
83 void get_swapped_functions(std::set<irep_idt> &dest) const;
84
85protected:
94
96 static std::map<
98 std::
99 pair<irep_idt, std::pair<dfcc_contract_modet, dfcc_loop_contract_modet>>>
101
102 void swap_and_wrap(
103 const dfcc_contract_modet contract_mode,
104 const dfcc_loop_contract_modet loop_contract_mode,
105 const irep_idt &function_id,
106 const irep_idt &contract_id,
107 std::set<irep_idt> &function_pointer_contracts,
108 bool allow_recursive_calls);
109
112 void check_contract(
113 const dfcc_loop_contract_modet loop_contract_mode,
114 const irep_idt &function_id,
115 const irep_idt &contract_id,
116 std::set<irep_idt> &function_pointer_contracts,
117 bool allow_recursive_calls);
118
122 const irep_idt &function_id,
123 const irep_idt &contract_id,
124 std::set<irep_idt> &function_pointer_contracts);
125};
126#endif
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition c_expr.h:232
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.
This class rewrites GOTO functions that use the built-ins:
void swap_and_wrap(const dfcc_contract_modet contract_mode, const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
message_handlert & message_handler
dfcc_spec_functionst & spec_functions
dfcc_libraryt & library
void swap_and_wrap_check(const dfcc_loop_contract_modet loop_contract_mode, const irep_idt &function_id, const irep_idt &contract_id, std::set< irep_idt > &function_pointer_contracts, bool allow_recursive_calls)
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.
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...
static std::map< irep_idt, std::pair< irep_idt, std::pair< dfcc_contract_modet, dfcc_loop_contract_modet > > > cache
remember all functions that were swapped/wrapped and in which mode
void check_contract(const dfcc_loop_contract_modet loop_contract_mode, 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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
@ NONE
Do not apply loop contracts.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Goto Programs with Functions.
API to expression classes.
Pre-defined types.
dstringt irep_idt