CBMC
Loading...
Searching...
No Matches
dfcc.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
9#include "dfcc.h"
10
11#include <util/config.h>
12#include <util/prefix.h>
13#include <util/string_utils.h>
14
17
25
27#include "dfcc_utils.h"
28
31 std::string reason,
32 std::string correct_format)
33 : cprover_exception_baset(std::move(reason)),
34 correct_format(std::move(correct_format))
35{
36}
37
39{
40 std::string res;
41
42 res += "Invalid function-contract mapping";
43 res += "\nReason: " + reason;
44
45 if(!correct_format.empty())
46 {
47 res += "\nFormat: " + correct_format;
48 }
49
50 return res;
51}
52
53static std::pair<irep_idt, irep_idt>
55{
56 auto const correct_format_message =
57 "the format for function and contract pairs is "
58 "`<function_name>[/<contract_name>]`";
59
60 std::string cli_flag_str = id2string(cli_flag);
61
62 auto split = split_string(cli_flag_str, '/', true, false);
63
64 if(split.size() == 1)
65 {
66 return std::make_pair(cli_flag, cli_flag);
67 }
68 else if(split.size() == 2)
69 {
70 auto function_name = split[0];
71 if(function_name.empty())
72 {
74 "couldn't find function name before '/' in '" + cli_flag_str + "'",
76 }
77 auto contract_name = split[1];
78 if(contract_name.empty())
79 {
81 "couldn't find contract name after '/' in '" + cli_flag_str + "'",
83 }
84 return std::make_pair(function_name, contract_name);
85 }
86 else
87 {
89 "couldn't parse '" + cli_flag_str + "'", correct_format_message};
90 }
91}
92
93void dfcc(
94 const optionst &options,
95 goto_modelt &goto_model,
96 const irep_idt &harness_id,
97 const std::optional<irep_idt> &to_check,
98 const bool allow_recursive_calls,
99 const std::set<irep_idt> &to_replace,
100 const loop_contract_configt loop_contract_config,
101 const std::set<std::string> &to_exclude_from_nondet_static,
102 message_handlert &message_handler)
103{
104 std::map<irep_idt, irep_idt> to_replace_map;
105 for(const auto &cli_flag : to_replace)
107
108 dfcct(
109 options,
110 goto_model,
111 harness_id,
112 to_check.has_value() ? parse_function_contract_pair(to_check.value())
113 : std::optional<std::pair<irep_idt, irep_idt>>{},
114 allow_recursive_calls,
116 loop_contract_config,
117 message_handler,
118 to_exclude_from_nondet_static);
119}
120
122 const optionst &options,
123 goto_modelt &goto_model,
124 const irep_idt &harness_id,
125 const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
126 const bool allow_recursive_calls,
127 const std::map<irep_idt, irep_idt> &to_replace,
128 const loop_contract_configt loop_contract_config,
129 message_handlert &message_handler,
130 const std::set<std::string> &to_exclude_from_nondet_static)
131 : options(options),
132 goto_model(goto_model),
133 harness_id(harness_id),
134 to_check(to_check),
135 allow_recursive_calls(allow_recursive_calls),
136 to_replace(to_replace),
137 loop_contract_config(loop_contract_config),
138 to_exclude_from_nondet_static(to_exclude_from_nondet_static),
139 message_handler(message_handler),
140 log(message_handler),
141 library(goto_model, message_handler),
142 ns(goto_model.symbol_table),
143 spec_functions(goto_model, message_handler, library),
144 contract_clauses_codegen(goto_model, message_handler, library),
145 instrument(
146 goto_model,
147 message_handler,
148 library,
149 spec_functions,
150 contract_clauses_codegen),
151 memory_predicates(goto_model, library, instrument, message_handler),
152 contract_handler(
153 goto_model,
154 message_handler,
155 library,
156 instrument,
157 memory_predicates,
158 spec_functions,
159 contract_clauses_codegen),
160 swap_and_wrap(
161 goto_model,
162 message_handler,
163 library,
164 instrument,
165 spec_functions,
166 contract_handler),
167 max_assigns_clause_size(0)
168{
170}
171
173{
174 // check that harness function exists
177 "Harness function '" + id2string(harness_id) +
178 "' either not found or has no body");
179
180 if(to_check.has_value())
181 {
182 auto pair = to_check.value();
185 "Function to check '" + id2string(pair.first) +
186 "' either not found or has no body");
187
188 // triggers signature compatibility checking
190
192 pair.first != harness_id,
193 "Function '" + id2string(pair.first) +
194 "' cannot be both be checked against a contract and be the harness");
195
197 pair.second != harness_id,
198 "Function '" + id2string(pair.first) +
199 "' cannot be both the contract to check and be the harness");
200
202 to_replace.find(pair.first) == to_replace.end(),
203 "Function '" + id2string(pair.first) +
204 "' cannot be both checked against contract and replaced by a contract");
205
208 "CPROVER function or builtin '" + id2string(pair.first) +
209 "' cannot be checked against a contract");
210 }
211
212 for(const auto &pair : to_replace)
213 {
214 // for functions to replace with contracts we don't require the replaced
215 // function to have a body because only the contract is actually used
218 "Function to replace '" + id2string(pair.first) + "' not found");
219
220 // triggers signature compatibility checking
222
224 pair.first != harness_id,
225 "Function '" + id2string(pair.first) +
226 "' cannot both be replaced with a contract and be the harness");
227
229 pair.second != harness_id,
230 "Function '" + id2string(pair.first) +
231 "' cannot both be the contract to use for replacement and be the "
232 "harness");
233 }
234}
235
237 std::set<irep_idt> &contract_symbols,
238 std::set<irep_idt> &other_symbols)
239{
240 std::set<irep_idt> called_functions;
245
246 // collect contract and other symbols
247 for(auto &entry : goto_model.symbol_table)
248 {
249 const symbolt &symbol = entry.second;
250
251 // not a function symbol
252 if(symbol.type.id() != ID_code || symbol.is_macro)
253 continue;
254
255 // is it a pure contract ?
256 const irep_idt &sym_name = symbol.name;
257 if(symbol.is_property && has_prefix(id2string(sym_name), "contract::"))
258 {
260 }
261 else if(called_functions.find(sym_name) != called_functions.end())
262 {
263 // it is not a contract
264 other_symbols.insert(sym_name);
265 }
266 }
267}
268
270{
271 // load the cprover library to make sure the model is complete
272 log.status() << "Loading CPROVER C library (" << config.ansi_c.arch << ")"
273 << messaget::eom;
276
277 // this must be done before loading the dfcc lib
279
280 // load the dfcc library before instrumentation starts
282
283 // disable checks on all library functions
285
286 // add C prover lib again to fetch any dependencies of the dfcc functions
289}
290
292{
293 // instrument the harness function
294 // load the cprover library to make sure the model is complete
295 log.status() << "Instrumenting harness function '" << harness_id << "'"
296 << messaget::eom;
297
300
302}
303
305{
306 std::set<irep_idt> predicates =
308 for(const auto &predicate : predicates)
309 {
310 log.debug() << "Memory predicate" << predicate << messaget::eom;
311 if(other_symbols.find(predicate) != other_symbols.end())
312 other_symbols.erase(predicate);
313 }
314}
315
317{
318 // swap-and-wrap checked functions with contracts
319 if(to_check.has_value())
320 {
321 const auto &pair = to_check.value();
322 const auto &wrapper_id = pair.first;
323 const auto &contract_id = pair.second;
324 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
325 << contract_id << "' in CHECK mode" << messaget::eom;
326
333
334 if(other_symbols.find(wrapper_id) != other_symbols.end())
336
337 // update max contract size
338 const std::size_t assigns_clause_size =
342 }
343}
344
346{
347 // swap-and-wrap replaced functions with contracts
348 for(const auto &pair : to_replace)
349 {
350 const auto &wrapper_id = pair.first;
351 const auto &contract_id = pair.second;
352 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
353 << contract_id << "' in REPLACE mode" << messaget::eom;
356
357 if(other_symbols.find(wrapper_id) != other_symbols.end())
359 }
360}
361
363{
364 std::set<irep_idt> swapped;
365 while(!function_pointer_contracts.empty())
366 {
367 std::set<irep_idt> new_contracts;
368 // swap-and-wrap function pointer contracts with themselves
369 for(const auto &fp_contract : function_pointer_contracts)
370 {
371 if(swapped.find(fp_contract) != swapped.end())
372 continue;
373
374 // contracts for function pointers must be replaced with themselves
375 // so we need to check that:
376 // - the symbol exists as a function symbol
377 // - the symbol exists as a pure contract symbol
378 // - the function symbol is not already swapped for contract checking
379 // - the function symbol is not already swapped with another contract for
380 // replacement
381
382 const auto str = id2string(fp_contract);
383
384 // Is it already swapped with another function for contract checking ?
386 !to_check.has_value() || to_check.value().first != str,
387 "Function '" + str +
388 "' used as contract for function pointer cannot be itself the object "
389 "of a contract check.");
390
391 // Is it already swapped with another function for contract checking ?
392 auto found = to_replace.find(str);
393 if(found != to_replace.end())
394 {
396 found->first == found->second,
397 "Function '" + str +
398 "' used as contract for function pointer already the object of a "
399 "contract replacement with '" +
400 id2string(found->second) + "'");
401 log.status() << "Function pointer contract '" << fp_contract
402 << "' already wrapped with itself in REPLACE mode"
403 << messaget::eom;
404 }
405 else
406 {
407 // we need to swap it with itself
410 "Function pointer contract '" + str + "' not found.");
411
412 // triggers signature compatibility checking
414
415 log.status() << "Wrapping function pointer contract '" << fp_contract
416 << "' with itself in REPLACE mode" << messaget::eom;
417
420 swapped.insert(fp_contract);
421
422 // remove it from the set of symbols to process
423 if(other_symbols.find(fp_contract) != other_symbols.end())
425 }
426 }
427 // process newly discovered contracts
429 }
430}
431
433{
434 // instrument all other remaining functions
435 for(const auto &function_id : other_symbols)
436 {
437 // Don't instrument CPROVER and internal functions
438 if(instrument.do_not_instrument(function_id))
439 {
440 continue;
441 }
442
443 log.status() << "Instrumenting '" << function_id << "'" << messaget::eom;
444
447 }
448
450}
451
453{
462
463 // take the max of function of loop contracts assigns clauses
467
468 log.status() << "Specializing cprover_contracts functions for assigns "
469 "clauses of at most "
470 << max_assigns_clause_size << " targets" << messaget::eom;
472
474
476
479
480 log.status() << "Removing unused functions" << messaget::eom;
481
482 // This can prune too many functions if function pointers have not been
483 // yet been removed or if the entry point is not defined.
484 // TODO: add a command line flag to tell the instrumentation to not prune
485 // a function.
488
489 // generate assert(0); assume(0); function bodies for all functions missing an
490 // implementation (other than ones containing __CPROVER in their name)
492 "assert-false-assume-false",
497 std::regex("(?!" CPROVER_PREFIX ").*"),
501 true);
503
505}
506
508{
509 // collect set of functions which are now instrumented
510 std::set<irep_idt> instrumented_functions;
513
514 log.status() << "Updating init function" << messaget::eom;
518
519 // Initialize the map of instrumented functions by adding extra instructions
520 // to the harness function
522 auto &body = init_function.body;
523 auto begin = body.instructions.begin();
526 instrumented_functions, begin->source_location(), payload);
527 body.destructive_insert(begin, payload);
528
529 // Define harness as the entry point, overriding any preexisting one.
530 log.status() << "Setting entry point to " << harness_id << messaget::eom;
531 // remove the CPROVER start function
534 // regenerate the CPROVER start function
540
542}
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
bool generate_ansi_c_start_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler, const c_object_factory_parameterst &object_factory_parameters)
Generate a _start function for a specific function.
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
struct configt::ansi_ct ansi_c
Base class for exceptions thrown in the cprover project.
Definition c_errors.h:64
std::string reason
The reason this exception was generated.
Definition c_errors.h:83
const symbolt & get_pure_contract_symbol(const irep_idt &contract_id, const std::optional< irep_idt > function_id_opt={})
Searches for a symbol named "contract::contract_id" in the symbol table.
const std::size_t get_assigns_clause_size(const irep_idt &contract_id)
Returns the size assigns clause of the given contract in number of targets.
void instrument_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
void get_instrumented_functions(std::set< irep_idt > &dest) const
Adds the names of instrumented functions to dest.
std::size_t get_max_assigns_clause_size() const
bool do_not_instrument(const irep_idt &id) const
True iff the symbol must not be instrumented because it is an internal symbol or a CPROVER symbol.
void instrument_harness_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
void add_instrumented_functions_map_init_instructions(const std::set< irep_idt > &instrumented_functions, const source_locationt &source_location, goto_programt &dest)
Generates instructions to initialize the instrumented function map symbol from the given set of instr...
void inhibit_front_end_builtins()
Adds an ASSERT(false) body to all front-end functions __CPROVER_object_whole __CPROVER_object_upto __...
void disable_checks()
Adds "checked" pragmas to instructions of all library functions instructions.
void specialize(const std::size_t contract_assigns_size_hint)
Specializes the library by unwinding loops in library functions to the given assigns clause size.
void load(std::set< irep_idt > &to_instrument)
After calling this function, all library types and functions are present in the the goto_model.
std::set< irep_idt > lift_predicates(std::set< irep_idt > &discovered_function_pointer_contracts)
Collects and lifts all user-defined memory predicates.
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)
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.
Entry point into the contracts transformation.
Definition dfcc.h:116
goto_modelt & goto_model
Definition dfcc.h:168
std::set< irep_idt > function_pointer_contracts
Definition dfcc.h:196
const optionst & options
Definition dfcc.h:167
std::set< irep_idt > pure_contract_symbols
Definition dfcc.h:194
void instrument_harness_function()
Definition dfcc.cpp:291
void instrument_other_functions()
Definition dfcc.cpp:432
const loop_contract_configt loop_contract_config
Definition dfcc.h:173
void reinitialize_model()
Re-initialise the GOTO model.
Definition dfcc.cpp:507
const std::set< std::string > & to_exclude_from_nondet_static
Definition dfcc.h:174
void link_model_and_load_dfcc_library()
Definition dfcc.cpp:269
dfcct(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< std::pair< irep_idt, irep_idt > > &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const loop_contract_configt loop_contract_config, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static)
Class constructor.
Definition dfcc.cpp:121
dfcc_swap_and_wrapt swap_and_wrap
Definition dfcc.h:187
dfcc_lift_memory_predicatest memory_predicates
Definition dfcc.h:185
void wrap_checked_function()
Definition dfcc.cpp:316
void lift_memory_predicates()
Definition dfcc.cpp:304
messaget log
Definition dfcc.h:176
const std::optional< std::pair< irep_idt, irep_idt > > & to_check
Definition dfcc.h:170
void check_transform_goto_model_preconditions()
Checks preconditions on arguments of transform_goto_model.
Definition dfcc.cpp:172
std::size_t max_assigns_clause_size
Tracks the maximum number of targets in any assigns clause handled in the transformation (used to spe...
Definition dfcc.h:191
void transform_goto_model()
Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame co...
Definition dfcc.cpp:452
dfcc_instrumentt instrument
Definition dfcc.h:184
dfcc_libraryt library
Definition dfcc.h:180
void wrap_replaced_functions()
Definition dfcc.cpp:345
message_handlert & message_handler
Definition dfcc.h:175
const irep_idt & harness_id
Definition dfcc.h:169
const bool allow_recursive_calls
Definition dfcc.h:171
std::set< irep_idt > other_symbols
Definition dfcc.h:195
dfcc_contract_handlert contract_handler
Definition dfcc.h:186
const std::map< irep_idt, irep_idt > & to_replace
Definition dfcc.h:172
void partition_function_symbols(std::set< irep_idt > &pure_contract_symbols, std::set< irep_idt > &other_symbols)
Partitions the function symbols of the symbol table into pure contracts and other function symbols sy...
Definition dfcc.cpp:236
void wrap_discovered_function_pointer_contracts()
Definition dfcc.cpp:362
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition goto_model.h:95
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.
Exception thrown for bad function/contract specification pairs passed on the CLI.
Definition dfcc.h:73
invalid_function_contract_pair_exceptiont(std::string reason, std::string correct_format="")
Definition dfcc.cpp:30
std::string what() const override
A human readable description of what went wrong.
Definition dfcc.cpp:38
const irep_idt & id() const
Definition irep.h:388
mstreamt & debug() const
Definition message.h:421
message_handlert & get_message_handler()
Definition message.h:183
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
const symbolst & symbols
Read-only field, used to look up symbols given their names.
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
Symbol table entry.
Definition symbol.h:28
bool is_macro
Definition symbol.h:62
bool is_property
Definition symbol.h:67
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
static std::pair< irep_idt, irep_idt > parse_function_contract_pair(const irep_idt &cli_flag)
Definition dfcc.cpp:54
Main class orchestrating the the whole program transformation for function contracts with Dynamic Fra...
Collects all user-defined predicates that call functions is_fresh, pointer_in_range,...
Dynamic frame condition checking utility functions.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler, bool ignore_no_match)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
void dfcc(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const std::optional< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const loop_contract_configt loop_contract_config, const std::set< std::string > &to_exclude_from_nondet_static, message_handlert &message_handler)
Applies function contracts transformation to GOTO model, using the dynamic frame condition checking a...
Definition dfcc.cpp:93
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
double log(double x)
Definition math.c:2449
STL namespace.
static void nondet_static(const namespacet &ns, goto_modelt &goto_model, const irep_idt &fct_name)
Nondeterministically initializes global scope variables in a goto-function.
Nondeterministically initializes global scope variables, except for constants (such as string literal...
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
void remove_unused_functions(goto_modelt &goto_model, message_handlert &message_handler)
void find_used_functions(const irep_idt &start, goto_functionst &functions, std::set< irep_idt > &seen)
Unused function removal.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
Definition invariant.h:464
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
Loop contract configurations.