cprover
Loading...
Searching...
No Matches
dfcc_swap_and_wrap.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmarsd@amazon.com
6
7\*******************************************************************/
8
10
11#include <util/config.h>
12#include <util/expr_util.h>
13#include <util/format_expr.h>
14#include <util/format_type.h>
15#include <util/fresh_symbol.h>
18#include <util/namespace.h>
19#include <util/optional.h>
20#include <util/pointer_expr.h>
23#include <util/std_expr.h>
24
31
32#include <ansi-c/c_expr.h>
37
39 goto_modelt &goto_model,
40 message_handlert &message_handler,
41 dfcc_libraryt &library,
42 dfcc_instrumentt &instrument,
43 dfcc_spec_functionst &spec_functions,
44 dfcc_contract_handlert &contract_handler)
45 : goto_model(goto_model),
46 message_handler(message_handler),
47 log(message_handler),
48 library(library),
49 instrument(instrument),
50 spec_functions(spec_functions),
51 contract_handler(contract_handler),
52 ns(goto_model.symbol_table)
53{
54}
55
56// static map
57std::map<
59 std::pair<irep_idt, std::pair<dfcc_contract_modet, dfcc_loop_contract_modet>>>
61
63 const dfcc_contract_modet contract_mode,
64 const dfcc_loop_contract_modet loop_contract_mode,
65 const irep_idt &function_id,
66 const irep_idt &contract_id,
67 std::set<irep_idt> &function_pointer_contracts,
68 bool allow_recursive_calls)
69{
70 auto pair = cache.insert(
71 {function_id, {contract_id, {contract_mode, loop_contract_mode}}});
72 auto inserted = pair.second;
73
74 if(!inserted)
75 {
76 irep_idt old_contract_id = pair.first->second.first;
77 dfcc_contract_modet old_contract_mode = pair.first->second.second.first;
79 pair.first->second.second.second;
80
81 // different swap already performed, abort (should be unreachable)
82 if(
83 old_contract_id != contract_id || old_contract_mode != contract_mode ||
84 old_loop_contract_mode != loop_contract_mode)
85 {
86 std::ostringstream err_msg;
87 err_msg << "DFCC: multiple attempts to swap and wrap function '"
88 << function_id << "':\n";
89 err_msg << "- with '" << old_contract_id << "' in "
92 << "\n";
93 err_msg << "- with '" << contract_id << "' in "
94 << dfcc_contract_mode_to_string(contract_mode) << " "
95 << dfcc_loop_contract_mode_to_string(loop_contract_mode) << "\n";
97 }
98 // same swap already performed
99 return;
100 }
101
102 // actually perform the translation
103 switch(contract_mode)
104 {
106 {
108 loop_contract_mode,
109 function_id,
111 function_pointer_contracts,
112 allow_recursive_calls);
113 break;
114 }
116 {
117 replace_with_contract(function_id, contract_id, function_pointer_contracts);
118 break;
119 }
120 }
121}
122
123void dfcc_swap_and_wrapt::get_swapped_functions(std::set<irep_idt> &dest) const
124{
125 for(const auto &it : dfcc_swap_and_wrapt::cache)
126 {
127 dest.insert(it.first);
128 }
129}
130
156 const dfcc_loop_contract_modet loop_contract_mode,
157 const irep_idt &function_id,
158 const irep_idt &contract_id,
159 std::set<irep_idt> &function_pointer_contracts,
160 bool allow_recursive_calls)
161{
162 // all code generation needs to run on functions with unmodified signatures
163 const irep_idt &wrapper_id = function_id;
164 const irep_idt wrapped_id =
165 id2string(wrapper_id) + "_wrapped_for_contract_checking";
167
168 // wrapper body
169 goto_programt body;
170
171 const auto &wrapper_symbol =
173
176 bool_typet(),
177 id2string(function_id),
178 "__contract_check_in_progress",
179 wrapper_symbol.location,
180 wrapper_symbol.mode,
181 wrapper_symbol.module,
182 false_exprt())
183 .symbol_expr();
184
187 bool_typet(),
188 id2string(function_id),
189 "__contract_checked_once",
190 wrapper_symbol.location,
191 wrapper_symbol.mode,
192 wrapper_symbol.module,
193 false_exprt())
194 .symbol_expr();
195
197 check_started, wrapper_symbol.location));
198
199 // At most a single top level call to the checked function in any execution
200
201 // Recursive calls within a contract check correspond to
202 // `check_started && !check_completed` and are allowed.
203
204 // Any other call occuring with `check_completed` true is forbidden.
205 source_locationt sl(wrapper_symbol.location);
206 sl.set_function(wrapper_symbol.name);
207 sl.set_property_class("single_top_level_call");
208 sl.set_comment(
209 "Only a single top-level call to function " + id2string(function_id) +
210 " when checking contract " + id2string(contract_id));
213 check_started, true_exprt(), wrapper_symbol.location));
214
217 function_id,
218 "__write_set_to_check",
220
227 body,
228 function_pointer_contracts);
229
231 check_completed, true_exprt(), wrapper_symbol.location));
233 check_started, false_exprt(), wrapper_symbol.location));
234
235 // unconditionally Jump to the end after the check
236 auto goto_end_function =
237 body.add(goto_programt::make_incomplete_goto(wrapper_symbol.location));
238
239 // Jump to the replacement section if check already in progress
241 body.add(goto_programt::make_skip(wrapper_symbol.location));
243
244 if(allow_recursive_calls)
245 {
252 body,
253 function_pointer_contracts);
254 }
255 else
256 {
257 source_locationt sl(wrapper_symbol.location);
258 sl.set_function(wrapper_symbol.name);
259 sl.set_property_class("no_recursive_call");
260 sl.set_comment(
261 "No recursive call to function " + id2string(function_id) +
262 " when checking contract " + id2string(contract_id));
264 body.add(
265 goto_programt::make_assumption(false_exprt(), wrapper_symbol.location));
266 }
267
268 auto end_function_label =
269 body.add(goto_programt::make_end_function(wrapper_symbol.location));
271
272 // write the body to the GOTO function
273 goto_model.goto_functions.function_map.at(function_id).body.swap(body);
274
275 // extend the signature of the wrapper function with the write set parameter
277
279
280 // instrument the wrapped function
282 wrapped_id, wrapper_id, loop_contract_mode, function_pointer_contracts);
283
285}
286
288 const irep_idt &function_id,
289 const irep_idt &contract_id,
290 std::set<irep_idt> &function_pointer_contracts)
291{
292 const irep_idt &wrapper_id = function_id;
293 const irep_idt wrapped_id =
294 id2string(function_id) + "_wrapped_for_replacement_with_contract";
296
299 function_id,
300 "__write_set_to_check",
302
303 goto_programt body;
304
311 body,
312 function_pointer_contracts);
313
316 .location));
317
319
320 // write the body to the GOTO function
321 goto_model.goto_functions.function_map.at(function_id).body.swap(body);
322
323 // extend the signature with the new write set parameter
325}
API to expression classes that are internal to the C frontend.
Classes providing CFG-based information about symbols to guide simplifications in function and loop a...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
The Boolean type.
Definition std_types.h:36
A contract is represented by a function declaration or definition with contract clauses attached to i...
void add_contract_instructions(const dfcc_contract_modet contract_mode, const irep_idt &wrapper_id, const irep_idt &wrapped_id, const irep_idt &contract_id, const symbolt &wrapper_write_set_symbol, goto_programt &dest, std::set< irep_idt > &function_pointer_contracts)
Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the f...
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
void instrument_wrapped_function(const irep_idt &wrapped_function_id, const irep_idt &initial_function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and inserting frame condition chec...
Class interface to library types and functions defined in cprover_contracts.c.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
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)
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 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
The Boolean constant false.
Definition std_expr.h:3017
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Thrown when user-provided input cannot be processed.
Boolean negation.
Definition std_expr.h:2278
The Boolean constant true.
Definition std_expr.h:3008
std::string dfcc_contract_mode_to_string(const dfcc_contract_modet mode)
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
@ CAR_SET_PTR
type of pointers to sets of CAR
std::string dfcc_loop_contract_mode_to_string(const dfcc_loop_contract_modet mode)
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
Given a function_id and contract_id, swaps its body to a function with a fresh mangled name,...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
Goto Programs with Functions.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
API to expression classes for 'mathematical' expressions.
Mathematical types.
API to expression classes for Pointers.
Pointer Logic.
Various predicates over pointers in programs.
Program Transformation.
API to expression classes.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static const symbolt & create_new_parameter_symbol(symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
Creates a new parameter symbol for the given function_id.
static void wrap_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &wrapped_function_id)
Given a function to wrap foo and a new name wrapped_foo
static const symbolt & create_static_symbol(symbol_table_baset &, const typet &type, const std::string &prefix, const std::string &base_name, const source_locationt &source_location, const irep_idt &mode, const irep_idt &module, const exprt &initial_value, const bool no_nondet_initialization=true)
Adds a new static symbol named prefix::base_name of type type with value initial_value in the symbol ...
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
dstringt irep_idt