cprover
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/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/prefix.h>
23#include <util/std_expr.h>
24#include <util/string_utils.h>
25
32
34#include <ansi-c/c_expr.h>
43#include <langapi/language.h>
45#include <langapi/mode.h>
47
49
58
60{
61 std::string res;
62
63 res += "Invalid function-contract mapping";
64 res += "\nReason: " + reason;
65
66 if(!correct_format.empty())
67 {
68 res += "\nFormat: " + correct_format;
69 }
70
71 return res;
72}
73
74static std::pair<irep_idt, irep_idt>
76{
77 auto const correct_format_message =
78 "the format for function and contract pairs is "
79 "`<function_name>[/<contract_name>]`";
80
81 std::string cli_flag_str = id2string(cli_flag);
82
83 auto split = split_string(cli_flag_str, '/', true, false);
84
85 if(split.size() == 1)
86 {
87 return std::make_pair(cli_flag, cli_flag);
88 }
89 else if(split.size() == 2)
90 {
91 auto function_name = split[0];
92 if(function_name.empty())
93 {
95 "couldn't find function name before '/' in '" + cli_flag_str + "'",
96 correct_format_message};
97 }
98 auto contract_name = split[1];
99 if(contract_name.empty())
100 {
102 "couldn't find contract name after '/' in '" + cli_flag_str + "'",
103 correct_format_message};
104 }
105 return std::make_pair(function_name, contract_name);
106 }
107 else
108 {
110 "couldn't parse '" + cli_flag_str + "'", correct_format_message};
111 }
112}
113
114void dfcc(
115 const optionst &options,
116 goto_modelt &goto_model,
117 const irep_idt &harness_id,
118 const std::optional<irep_idt> &to_check,
119 const bool allow_recursive_calls,
120 const std::set<irep_idt> &to_replace,
121 const loop_contract_configt loop_contract_config,
122 const std::set<std::string> &to_exclude_from_nondet_static,
123 message_handlert &message_handler)
124{
125 std::map<irep_idt, irep_idt> to_replace_map;
126 for(const auto &cli_flag : to_replace)
127 to_replace_map.insert(parse_function_contract_pair(cli_flag));
128
129 dfcct(
130 options,
131 goto_model,
132 harness_id,
133 to_check.has_value() ? parse_function_contract_pair(to_check.value())
134 : std::optional<std::pair<irep_idt, irep_idt>>{},
135 allow_recursive_calls,
136 to_replace_map,
137 loop_contract_config,
138 message_handler,
139 to_exclude_from_nondet_static);
140}
141
143 const optionst &options,
145 const irep_idt &harness_id,
146 const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
147 const bool allow_recursive_calls,
148 const std::map<irep_idt, irep_idt> &to_replace,
151 const std::set<std::string> &to_exclude_from_nondet_static)
152 : options(options),
163 ns(goto_model.symbol_table),
169 library,
176 library,
184 library,
189{
191}
192
194{
195 // check that harness function exists
198 "Harness function '" + id2string(harness_id) +
199 "' either not found or has no body");
200
201 if(to_check.has_value())
202 {
203 auto pair = to_check.value();
206 "Function to check '" + id2string(pair.first) +
207 "' either not found or has no body");
208
209 // triggers signature compatibility checking
210 contract_handler.get_pure_contract_symbol(pair.second, pair.first);
211
213 pair.first != harness_id,
214 "Function '" + id2string(pair.first) +
215 "' cannot be both be checked against a contract and be the harness");
216
218 pair.second != harness_id,
219 "Function '" + id2string(pair.first) +
220 "' cannot be both the contract to check and be the harness");
221
223 to_replace.find(pair.first) == to_replace.end(),
224 "Function '" + id2string(pair.first) +
225 "' cannot be both checked against contract and replaced by a contract");
226
228 !instrument.do_not_instrument(pair.first),
229 "CPROVER function or builtin '" + id2string(pair.first) +
230 "' cannot be checked against a contract");
231 }
232
233 for(const auto &pair : to_replace)
234 {
235 // for functions to replace with contracts we don't require the replaced
236 // function to have a body because only the contract is actually used
239 "Function to replace '" + id2string(pair.first) + "' not found");
240
241 // triggers signature compatibility checking
242 contract_handler.get_pure_contract_symbol(pair.second, pair.first);
243
245 pair.first != harness_id,
246 "Function '" + id2string(pair.first) +
247 "' cannot both be replaced with a contract and be the harness");
248
250 pair.second != harness_id,
251 "Function '" + id2string(pair.first) +
252 "' cannot both be the contract to use for replacement and be the "
253 "harness");
254 }
255}
256
258 std::set<irep_idt> &contract_symbols,
259 std::set<irep_idt> &other_symbols)
260{
261 std::set<irep_idt> called_functions;
264 goto_model.goto_functions,
265 called_functions);
266
267 // collect contract and other symbols
268 for(auto &entry : goto_model.symbol_table)
269 {
270 const symbolt &symbol = entry.second;
271
272 // not a function symbol
273 if(symbol.type.id() != ID_code || symbol.is_macro)
274 continue;
275
276 // is it a pure contract ?
277 const irep_idt &sym_name = symbol.name;
278 if(symbol.is_property && has_prefix(id2string(sym_name), "contract::"))
279 {
280 contract_symbols.insert(sym_name);
281 }
282 else if(called_functions.find(sym_name) != called_functions.end())
283 {
284 // it is not a contract
285 other_symbols.insert(sym_name);
286 }
287 }
288}
289
291{
292 // load the cprover library to make sure the model is complete
293 log.status() << "Loading CPROVER C library (" << config.ansi_c.arch << ")"
294 << messaget::eom;
296 goto_model, log.get_message_handler(), cprover_c_library_factory);
297
298 // this must be done before loading the dfcc lib
300
301 // load the dfcc library before instrumentation starts
303
304 // disable checks on all library functions
305 library.disable_checks();
306
307 // add C prover lib again to fetch any dependencies of the dfcc functions
309 goto_model, log.get_message_handler(), cprover_c_library_factory);
310}
311
313{
314 // instrument the harness function
315 // load the cprover library to make sure the model is complete
316 log.status() << "Instrumenting harness function '" << harness_id << "'"
317 << messaget::eom;
318
319 instrument.instrument_harness_function(
321
323}
324
326{
327 std::set<irep_idt> predicates =
329 for(const auto &predicate : predicates)
330 {
331 log.debug() << "Memory predicate" << predicate << messaget::eom;
332 if(other_symbols.find(predicate) != other_symbols.end())
333 other_symbols.erase(predicate);
334 }
335}
336
338{
339 // swap-and-wrap checked functions with contracts
340 if(to_check.has_value())
341 {
342 const auto &pair = to_check.value();
343 const auto &wrapper_id = pair.first;
344 const auto &contract_id = pair.second;
345 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
346 << contract_id << "' in CHECK mode" << messaget::eom;
347
348 swap_and_wrap.swap_and_wrap_check(
350 wrapper_id,
351 contract_id,
354
355 if(other_symbols.find(wrapper_id) != other_symbols.end())
356 other_symbols.erase(wrapper_id);
357
358 // update max contract size
359 const std::size_t assigns_clause_size =
360 contract_handler.get_assigns_clause_size(contract_id);
361 if(assigns_clause_size > max_assigns_clause_size)
362 max_assigns_clause_size = assigns_clause_size;
363 }
364}
365
367{
368 // swap-and-wrap replaced functions with contracts
369 for(const auto &pair : to_replace)
370 {
371 const auto &wrapper_id = pair.first;
372 const auto &contract_id = pair.second;
373 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
374 << contract_id << "' in REPLACE mode" << messaget::eom;
375 swap_and_wrap.swap_and_wrap_replace(
376 wrapper_id, contract_id, function_pointer_contracts);
377
378 if(other_symbols.find(wrapper_id) != other_symbols.end())
379 other_symbols.erase(wrapper_id);
380 }
381}
382
384{
385 std::set<irep_idt> swapped;
386 while(!function_pointer_contracts.empty())
387 {
388 std::set<irep_idt> new_contracts;
389 // swap-and-wrap function pointer contracts with themselves
390 for(const auto &fp_contract : function_pointer_contracts)
391 {
392 if(swapped.find(fp_contract) != swapped.end())
393 continue;
394
395 // contracts for function pointers must be replaced with themselves
396 // so we need to check that:
397 // - the symbol exists as a function symbol
398 // - the symbol exists as a pure contract symbol
399 // - the function symbol is not already swapped for contract checking
400 // - the function symbol is not already swapped with another contract for
401 // replacement
402
403 const auto str = id2string(fp_contract);
404
405 // Is it already swapped with another function for contract checking ?
407 !to_check.has_value() || to_check.value().first != str,
408 "Function '" + str +
409 "' used as contract for function pointer cannot be itself the object "
410 "of a contract check.");
411
412 // Is it already swapped with another function for contract checking ?
413 auto found = to_replace.find(str);
414 if(found != to_replace.end())
415 {
417 found->first == found->second,
418 "Function '" + str +
419 "' used as contract for function pointer already the object of a "
420 "contract replacement with '" +
421 id2string(found->second) + "'");
422 log.status() << "Function pointer contract '" << fp_contract
423 << "' already wrapped with itself in REPLACE mode"
424 << messaget::eom;
425 }
426 else
427 {
428 // we need to swap it with itself
431 "Function pointer contract '" + str + "' not found.");
432
433 // triggers signature compatibility checking
434 contract_handler.get_pure_contract_symbol(str);
435
436 log.status() << "Wrapping function pointer contract '" << fp_contract
437 << "' with itself in REPLACE mode" << messaget::eom;
438
439 swap_and_wrap.swap_and_wrap_replace(
440 fp_contract, fp_contract, new_contracts);
441 swapped.insert(fp_contract);
442
443 // remove it from the set of symbols to process
444 if(other_symbols.find(fp_contract) != other_symbols.end())
445 other_symbols.erase(fp_contract);
446 }
447 }
448 // process newly discovered contracts
449 function_pointer_contracts = new_contracts;
450 }
451}
452
454{
455 // instrument all other remaining functions
456 for(const auto &function_id : other_symbols)
457 {
458 // Don't instrument CPROVER and internal functions
459 if(instrument.do_not_instrument(function_id))
460 {
461 continue;
462 }
463
464 log.status() << "Instrumenting '" << function_id << "'" << messaget::eom;
465
466 instrument.instrument_function(
468 }
469
470 goto_model.goto_functions.update();
471}
472
474{
483
484 // take the max of function of loop contracts assigns clauses
485 auto assigns_clause_size = instrument.get_max_assigns_clause_size();
486 if(assigns_clause_size > max_assigns_clause_size)
487 max_assigns_clause_size = assigns_clause_size;
488
489 log.status() << "Specializing cprover_contracts functions for assigns "
490 "clauses of at most "
491 << max_assigns_clause_size << " targets" << messaget::eom;
493
494 library.inhibit_front_end_builtins();
495
496 goto_model.goto_functions.update();
497
499 goto_model.goto_functions.update();
500
501 log.status() << "Removing unused functions" << messaget::eom;
502
503 // This can prune too many functions if function pointers have not been
504 // yet been removed or if the entry point is not defined.
505 // TODO: add a command line flag to tell the instrumentation to not prune
506 // a function.
508 goto_model.goto_functions.update();
509
510 // generate assert(0); assume(0); function bodies for all functions missing an
511 // implementation (other than ones containing __CPROVER in their name)
512 auto generate_implementation = generate_function_bodies_factory(
513 "assert-false-assume-false",
515 goto_model.symbol_table,
518 std::regex("(?!" CPROVER_PREFIX ").*"),
519 *generate_implementation,
522 goto_model.goto_functions.update();
523
525}
526
528{
529 // collect set of functions which are now instrumented
530 std::set<irep_idt> instrumented_functions;
531 instrument.get_instrumented_functions(instrumented_functions);
532 swap_and_wrap.get_swapped_functions(instrumented_functions);
533
534 log.status() << "Updating init function" << messaget::eom;
535 if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
538
539 // Initialize the map of instrumented functions by adding extra instructions
540 // to the harness function
541 auto &init_function = goto_model.goto_functions.function_map[harness_id];
542 auto &body = init_function.body;
543 auto begin = body.instructions.begin();
544 goto_programt payload;
545 library.add_instrumented_functions_map_init_instructions(
546 instrumented_functions, begin->source_location(), payload);
547 body.destructive_insert(begin, payload);
548
549 // Define harness as the entry point, overriding any preexisting one.
550 log.status() << "Setting entry point to " << harness_id << messaget::eom;
551 // remove the CPROVER start function
552 goto_model.symbol_table.erase(
553 goto_model.symbol_table.symbols.find(goto_functionst::entry_point()));
554 // regenerate the CPROVER start function
557 goto_model.symbol_table,
560
561 goto_model.goto_functions.update();
562}
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
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...
cprover_exception_baset(std::string reason)
This constructor is marked protected to ensure this class isn't used directly.
Definition c_errors.h:76
std::string reason
The reason this exception was generated.
Definition c_errors.h:83
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
dfcc_spec_functionst spec_functions
Definition dfcc.h:182
void instrument_harness_function()
Definition dfcc.cpp:312
void instrument_other_functions()
Definition dfcc.cpp:453
const loop_contract_configt loop_contract_config
Definition dfcc.h:173
void reinitialize_model()
Re-initialise the GOTO model.
Definition dfcc.cpp:527
const std::set< std::string > & to_exclude_from_nondet_static
Definition dfcc.h:174
void link_model_and_load_dfcc_library()
Definition dfcc.cpp:290
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:142
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:337
void lift_memory_predicates()
Definition dfcc.cpp:325
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:193
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:473
dfcc_instrumentt instrument
Definition dfcc.h:184
dfcc_libraryt library
Definition dfcc.h:180
void wrap_replaced_functions()
Definition dfcc.cpp:366
message_handlert & message_handler
Definition dfcc.h:175
const irep_idt & harness_id
Definition dfcc.h:169
dfcc_contract_clauses_codegent contract_clauses_codegen
Definition dfcc.h:183
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:257
void wrap_discovered_function_pointer_contracts()
Definition dfcc.cpp:383
namespacet ns
Definition dfcc.h:181
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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:51
std::string what() const override
A human readable description of what went wrong.
Definition dfcc.cpp:59
const irep_idt & id() const
Definition irep.h:388
static eomt eom
Definition message.h:289
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:75
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,...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
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)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
Goto Programs with Functions.
Goto Programs with Functions.
Function Inlining This gives a number of different interfaces to the function inlining functionality ...
Symbol Table + CFG.
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:114
Initialize a Goto Program.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Abstract interface to support a programming language.
API to expression classes for 'mathematical' expressions.
Mathematical types.
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...
API to expression classes for Pointers.
Pointer Logic.
Various predicates over pointers in programs.
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
API to expression classes.
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.
dstringt irep_idt