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;
78 dfcc_loop_contract_modet old_loop_contract_mode =
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 "
90 << dfcc_contract_mode_to_string(old_contract_mode) << " "
91 << dfcc_loop_contract_mode_to_string(old_loop_contract_mode)
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";
96 throw invalid_input_exceptiont(err_msg.str());
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,
110 contract_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";
166 dfcc_utilst::wrap_function(goto_model, wrapper_id, wrapped_id);
167
168 // wrapper body
169 goto_programt body;
170
171 const auto &wrapper_symbol =
173
174 auto check_started = dfcc_utilst::create_static_symbol(
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
185 auto check_completed = dfcc_utilst::create_static_symbol(
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
196 auto check_started_goto = body.add(goto_programt::make_incomplete_goto(
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));
211 body.add(goto_programt::make_assertion(not_exprt(check_completed), sl));
213 check_started, true_exprt(), wrapper_symbol.location));
214
215 const auto write_set_symbol = dfcc_utilst::create_new_parameter_symbol(
217 function_id,
218 "__write_set_to_check",
220
223 wrapper_id,
224 wrapped_id,
225 contract_id,
226 write_set_symbol,
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
240 auto contract_replacement_label =
241 body.add(goto_programt::make_skip(wrapper_symbol.location));
242 check_started_goto->complete_goto(contract_replacement_label);
243
244 if(allow_recursive_calls)
245 {
248 wrapper_id,
249 wrapped_id,
250 contract_id,
251 write_set_symbol,
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));
270 goto_end_function->complete_goto(end_function_label);
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
276 dfcc_utilst::add_parameter(goto_model, write_set_symbol, function_id);
277
278 goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
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";
295 dfcc_utilst::wrap_function(goto_model, function_id, wrapped_id);
296
297 const auto write_set_symbol = dfcc_utilst::create_new_parameter_symbol(
299 function_id,
300 "__write_set_to_check",
302
303 goto_programt body;
304
307 wrapper_id,
308 wrapped_id,
309 contract_id,
310 write_set_symbol,
311 body,
312 function_pointer_contracts);
313
316 .location));
317
318 goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
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
324 dfcc_utilst::add_parameter(goto_model, write_set_symbol, function_id);
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...
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
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
void set_function(const irep_idt &function)
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
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