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/pointer_expr.h>
22#include <util/std_expr.h>
23
29
30#include <ansi-c/c_expr.h>
36
54
55// static map
56std::map<
58 std::pair<irep_idt, std::pair<dfcc_contract_modet, loop_contract_configt>>>
60
62 const dfcc_contract_modet contract_mode,
63 const loop_contract_configt &loop_contract_config,
64 const irep_idt &function_id,
65 const irep_idt &contract_id,
66 std::set<irep_idt> &function_pointer_contracts,
67 bool allow_recursive_calls)
68{
69 auto pair = cache.insert(
70 {function_id, {contract_id, {contract_mode, loop_contract_config}}});
71 auto inserted = pair.second;
72
73 if(!inserted)
74 {
75 irep_idt old_contract_id = pair.first->second.first;
76 dfcc_contract_modet old_contract_mode = pair.first->second.second.first;
77 loop_contract_configt old_loop_contract_config =
78 pair.first->second.second.second;
79
80 // different swap already performed, abort (should be unreachable)
81 if(
82 old_contract_id != contract_id || old_contract_mode != contract_mode ||
83 old_loop_contract_config != loop_contract_config)
84 {
85 std::ostringstream err_msg;
86 err_msg << "DFCC: multiple attempts to swap and wrap function '"
87 << function_id << "':\n";
88 err_msg << "- with '" << old_contract_id << "' in "
89 << dfcc_contract_mode_to_string(old_contract_mode) << " "
90 << old_loop_contract_config.to_string() << "\n";
91 err_msg << "- with '" << contract_id << "' in "
92 << dfcc_contract_mode_to_string(contract_mode) << " "
93 << loop_contract_config.to_string() << "\n";
94 throw invalid_input_exceptiont(err_msg.str());
95 }
96 // same swap already performed
97 return;
98 }
99
100 // actually perform the translation
101 switch(contract_mode)
102 {
104 {
106 loop_contract_config,
107 function_id,
108 contract_id,
109 function_pointer_contracts,
110 allow_recursive_calls);
111 break;
112 }
114 {
115 replace_with_contract(function_id, contract_id, function_pointer_contracts);
116 break;
117 }
118 }
119}
120
121void dfcc_swap_and_wrapt::get_swapped_functions(std::set<irep_idt> &dest) const
122{
123 for(const auto &it : dfcc_swap_and_wrapt::cache)
124 {
125 dest.insert(it.first);
126 }
127}
128
154 const loop_contract_configt &loop_contract_config,
155 const irep_idt &function_id,
156 const irep_idt &contract_id,
157 std::set<irep_idt> &function_pointer_contracts,
158 bool allow_recursive_calls)
159{
160 // all code generation needs to run on functions with unmodified signatures
161 const irep_idt &wrapper_id = function_id;
162 const irep_idt wrapped_id =
163 id2string(wrapper_id) + "_wrapped_for_contract_checking";
164 dfcc_utilst::wrap_function(goto_model, wrapper_id, wrapped_id);
165
166 // wrapper body
167 goto_programt body;
168
169 const auto &wrapper_symbol =
170 dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id);
171
172 auto check_started = dfcc_utilst::create_static_symbol(
173 goto_model.symbol_table,
174 bool_typet(),
175 id2string(function_id),
176 "__contract_check_in_progress",
177 wrapper_symbol.location,
178 wrapper_symbol.mode,
179 wrapper_symbol.module,
180 false_exprt())
181 .symbol_expr();
182
183 auto check_completed = dfcc_utilst::create_static_symbol(
184 goto_model.symbol_table,
185 bool_typet(),
186 id2string(function_id),
187 "__contract_checked_once",
188 wrapper_symbol.location,
189 wrapper_symbol.mode,
190 wrapper_symbol.module,
191 false_exprt())
192 .symbol_expr();
193
194 auto check_started_goto = body.add(goto_programt::make_incomplete_goto(
195 check_started, wrapper_symbol.location));
196
197 // At most a single top level call to the checked function in any execution
198
199 // Recursive calls within a contract check correspond to
200 // `check_started && !check_completed` and are allowed.
201
202 // Any other call occuring with `check_completed` true is forbidden.
203 source_locationt sl(wrapper_symbol.location);
204 sl.set_function(wrapper_symbol.name);
205 sl.set_property_class("single_top_level_call");
206 sl.set_comment(
207 "Only a single top-level call to function " + id2string(function_id) +
208 " when checking contract " + id2string(contract_id));
209 body.add(goto_programt::make_assertion(not_exprt(check_completed), sl));
211 check_started, true_exprt(), wrapper_symbol.location));
212
213 const auto write_set_symbol = dfcc_utilst::create_new_parameter_symbol(
214 goto_model.symbol_table,
215 function_id,
216 "__write_set_to_check",
218
219 contract_handler.add_contract_instructions(
221 wrapper_id,
222 wrapped_id,
223 contract_id,
224 write_set_symbol,
225 body,
226 function_pointer_contracts);
227
229 check_completed, true_exprt(), wrapper_symbol.location));
231 check_started, false_exprt(), wrapper_symbol.location));
232
233 // unconditionally Jump to the end after the check
234 auto goto_end_function =
235 body.add(goto_programt::make_incomplete_goto(wrapper_symbol.location));
236
237 // Jump to the replacement section if check already in progress
238 auto contract_replacement_label =
239 body.add(goto_programt::make_skip(wrapper_symbol.location));
240 check_started_goto->complete_goto(contract_replacement_label);
241
242 if(allow_recursive_calls)
243 {
244 contract_handler.add_contract_instructions(
246 wrapper_id,
247 wrapped_id,
248 contract_id,
249 write_set_symbol,
250 body,
251 function_pointer_contracts);
252 }
253 else
254 {
255 source_locationt sl(wrapper_symbol.location);
256 sl.set_function(wrapper_symbol.name);
257 sl.set_property_class("no_recursive_call");
258 sl.set_comment(
259 "No recursive call to function " + id2string(function_id) +
260 " when checking contract " + id2string(contract_id));
262 body.add(
263 goto_programt::make_assumption(false_exprt(), wrapper_symbol.location));
264 }
265
266 auto end_function_label =
267 body.add(goto_programt::make_end_function(wrapper_symbol.location));
268 goto_end_function->complete_goto(end_function_label);
269
270 // write the body to the GOTO function
271 goto_model.goto_functions.function_map.at(function_id).body.swap(body);
272
273 // extend the signature of the wrapper function with the write set parameter
274 dfcc_utilst::add_parameter(goto_model, write_set_symbol, function_id);
275
276 goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
277
278 // instrument the wrapped function
279 instrument.instrument_wrapped_function(
280 wrapped_id, wrapper_id, loop_contract_config, function_pointer_contracts);
281
282 goto_model.goto_functions.update();
283}
284
286 const irep_idt &function_id,
287 const irep_idt &contract_id,
288 std::set<irep_idt> &function_pointer_contracts)
289{
290 const irep_idt &wrapper_id = function_id;
291 const irep_idt wrapped_id =
292 id2string(function_id) + "_wrapped_for_replacement_with_contract";
293 dfcc_utilst::wrap_function(goto_model, function_id, wrapped_id);
294
295 const auto write_set_symbol = dfcc_utilst::create_new_parameter_symbol(
296 goto_model.symbol_table,
297 function_id,
298 "__write_set_to_check",
300
301 goto_programt body;
302
303 contract_handler.add_contract_instructions(
305 wrapper_id,
306 wrapped_id,
307 contract_id,
308 write_set_symbol,
309 body,
310 function_pointer_contracts);
311
313 dfcc_utilst::get_function_symbol(goto_model.symbol_table, wrapper_id)
314 .location));
315
316 goto_model.goto_functions.function_map.at(wrapper_id).make_hidden();
317
318 // write the body to the GOTO function
319 goto_model.goto_functions.function_map.at(function_id).body.swap(body);
320
321 // extend the signature with the new write set parameter
322 dfcc_utilst::add_parameter(goto_model, write_set_symbol, function_id);
323}
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...
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 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
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.
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)
The Boolean constant false.
Definition std_expr.h:3204
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:2459
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
void set_function(const irep_idt &function)
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:3195
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
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:44
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.
Loop contract configurations.
std::string to_string() const
dstringt irep_idt