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>
42#include <langapi/language.h>
44#include <langapi/mode.h>
46
48
57
59{
60 std::string res;
61
62 res += "Invalid function-contract mapping";
63 res += "\nReason: " + reason;
64
65 if(!correct_format.empty())
66 {
67 res += "\nFormat: " + correct_format;
68 }
69
70 return res;
71}
72
73static std::pair<irep_idt, irep_idt>
75{
76 auto const correct_format_message =
77 "the format for function and contract pairs is "
78 "`<function_name>[/<contract_name>]`";
79
80 std::string cli_flag_str = id2string(cli_flag);
81
82 auto split = split_string(cli_flag_str, '/', true, false);
83
84 if(split.size() == 1)
85 {
86 return std::make_pair(cli_flag, cli_flag);
87 }
88 else if(split.size() == 2)
89 {
90 auto function_name = split[0];
91 if(function_name.empty())
92 {
94 "couldn't find function name before '/' in '" + cli_flag_str + "'",
95 correct_format_message};
96 }
97 auto contract_name = split[1];
98 if(contract_name.empty())
99 {
101 "couldn't find contract name after '/' in '" + cli_flag_str + "'",
102 correct_format_message};
103 }
104 return std::make_pair(function_name, contract_name);
105 }
106 else
107 {
109 "couldn't parse '" + cli_flag_str + "'", correct_format_message};
110 }
111}
112
113void dfcc(
114 const optionst &options,
115 goto_modelt &goto_model,
116 const irep_idt &harness_id,
117 const std::optional<irep_idt> &to_check,
118 const bool allow_recursive_calls,
119 const std::set<irep_idt> &to_replace,
120 const loop_contract_configt loop_contract_config,
121 const std::set<std::string> &to_exclude_from_nondet_static,
122 message_handlert &message_handler)
123{
124 std::map<irep_idt, irep_idt> to_replace_map;
125 for(const auto &cli_flag : to_replace)
126 to_replace_map.insert(parse_function_contract_pair(cli_flag));
127
128 dfcct(
129 options,
130 goto_model,
131 harness_id,
132 to_check.has_value() ? parse_function_contract_pair(to_check.value())
133 : std::optional<std::pair<irep_idt, irep_idt>>{},
134 allow_recursive_calls,
135 to_replace_map,
136 loop_contract_config,
137 message_handler,
138 to_exclude_from_nondet_static);
139}
140
142 const optionst &options,
144 const irep_idt &harness_id,
145 const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
146 const bool allow_recursive_calls,
147 const std::map<irep_idt, irep_idt> &to_replace,
150 const std::set<std::string> &to_exclude_from_nondet_static)
151 : options(options),
162 ns(goto_model.symbol_table),
168 library,
175 library,
183 library,
188{
190}
191
193{
194 // check that harness function exists
197 "Harness function '" + id2string(harness_id) +
198 "' either not found or has no body");
199
200 if(to_check.has_value())
201 {
202 auto pair = to_check.value();
205 "Function to check '" + id2string(pair.first) +
206 "' either not found or has no body");
207
208 // triggers signature compatibility checking
209 contract_handler.get_pure_contract_symbol(pair.second, pair.first);
210
212 pair.first != harness_id,
213 "Function '" + id2string(pair.first) +
214 "' cannot be both be checked against a contract and be the harness");
215
217 pair.second != harness_id,
218 "Function '" + id2string(pair.first) +
219 "' cannot be both the contract to check and be the harness");
220
222 to_replace.find(pair.first) == to_replace.end(),
223 "Function '" + id2string(pair.first) +
224 "' cannot be both checked against contract and replaced by a contract");
225
227 !instrument.do_not_instrument(pair.first),
228 "CPROVER function or builtin '" + id2string(pair.first) +
229 "' cannot be checked against a contract");
230 }
231
232 for(const auto &pair : to_replace)
233 {
234 // for functions to replace with contracts we don't require the replaced
235 // function to have a body because only the contract is actually used
238 "Function to replace '" + id2string(pair.first) + "' not found");
239
240 // triggers signature compatibility checking
241 contract_handler.get_pure_contract_symbol(pair.second, pair.first);
242
244 pair.first != harness_id,
245 "Function '" + id2string(pair.first) +
246 "' cannot both be replaced with a contract and be the harness");
247
249 pair.second != harness_id,
250 "Function '" + id2string(pair.first) +
251 "' cannot both be the contract to use for replacement and be the "
252 "harness");
253 }
254}
255
257 std::set<irep_idt> &contract_symbols,
258 std::set<irep_idt> &other_symbols)
259{
260 // collect contract and other symbols
261 for(auto &entry : goto_model.symbol_table)
262 {
263 const symbolt &symbol = entry.second;
264
265 // not a function symbol
266 if(symbol.type.id() != ID_code || symbol.is_macro)
267 continue;
268
269 // is it a pure contract ?
270 const irep_idt &sym_name = symbol.name;
271 if(symbol.is_property && has_prefix(id2string(sym_name), "contract::"))
272 {
273 contract_symbols.insert(sym_name);
274 }
275 else
276 {
277 // it is not a contract
278 other_symbols.insert(sym_name);
279 }
280 }
281}
282
284{
285 // load the cprover library to make sure the model is complete
286 log.status() << "Loading CPROVER C library (" << config.ansi_c.arch << ")"
287 << messaget::eom;
289 goto_model, log.get_message_handler(), cprover_c_library_factory);
290
291 // this must be done before loading the dfcc lib
293
294 // load the dfcc library before instrumentation starts
296
297 // disable checks on all library functions
298 library.disable_checks();
299
300 // add C prover lib again to fetch any dependencies of the dfcc functions
302 goto_model, log.get_message_handler(), cprover_c_library_factory);
303}
304
306{
307 // instrument the harness function
308 // load the cprover library to make sure the model is complete
309 log.status() << "Instrumenting harness function '" << harness_id << "'"
310 << messaget::eom;
311
312 instrument.instrument_harness_function(
314
316}
317
319{
320 std::set<irep_idt> predicates =
322 for(const auto &predicate : predicates)
323 {
324 log.debug() << "Memory predicate" << predicate << messaget::eom;
325 if(other_symbols.find(predicate) != other_symbols.end())
326 other_symbols.erase(predicate);
327 }
328}
329
331{
332 // swap-and-wrap checked functions with contracts
333 if(to_check.has_value())
334 {
335 const auto &pair = to_check.value();
336 const auto &wrapper_id = pair.first;
337 const auto &contract_id = pair.second;
338 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
339 << contract_id << "' in CHECK mode" << messaget::eom;
340
341 swap_and_wrap.swap_and_wrap_check(
343 wrapper_id,
344 contract_id,
347
348 if(other_symbols.find(wrapper_id) != other_symbols.end())
349 other_symbols.erase(wrapper_id);
350
351 // update max contract size
352 const std::size_t assigns_clause_size =
353 contract_handler.get_assigns_clause_size(contract_id);
354 if(assigns_clause_size > max_assigns_clause_size)
355 max_assigns_clause_size = assigns_clause_size;
356 }
357}
358
360{
361 // swap-and-wrap replaced functions with contracts
362 for(const auto &pair : to_replace)
363 {
364 const auto &wrapper_id = pair.first;
365 const auto &contract_id = pair.second;
366 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
367 << contract_id << "' in REPLACE mode" << messaget::eom;
368 swap_and_wrap.swap_and_wrap_replace(
369 wrapper_id, contract_id, function_pointer_contracts);
370
371 if(other_symbols.find(wrapper_id) != other_symbols.end())
372 other_symbols.erase(wrapper_id);
373 }
374}
375
377{
378 std::set<irep_idt> swapped;
379 while(!function_pointer_contracts.empty())
380 {
381 std::set<irep_idt> new_contracts;
382 // swap-and-wrap function pointer contracts with themselves
383 for(const auto &fp_contract : function_pointer_contracts)
384 {
385 if(swapped.find(fp_contract) != swapped.end())
386 continue;
387
388 // contracts for function pointers must be replaced with themselves
389 // so we need to check that:
390 // - the symbol exists as a function symbol
391 // - the symbol exists as a pure contract symbol
392 // - the function symbol is not already swapped for contract checking
393 // - the function symbol is not already swapped with another contract for
394 // replacement
395
396 const auto str = id2string(fp_contract);
397
398 // Is it already swapped with another function for contract checking ?
400 !to_check.has_value() || to_check.value().first != str,
401 "Function '" + str +
402 "' used as contract for function pointer cannot be itself the object "
403 "of a contract check.");
404
405 // Is it already swapped with another function for contract checking ?
406 auto found = to_replace.find(str);
407 if(found != to_replace.end())
408 {
410 found->first == found->second,
411 "Function '" + str +
412 "' used as contract for function pointer already the object of a "
413 "contract replacement with '" +
414 id2string(found->second) + "'");
415 log.status() << "Function pointer contract '" << fp_contract
416 << "' already wrapped with itself in REPLACE mode"
417 << messaget::eom;
418 }
419 else
420 {
421 // we need to swap it with itself
424 "Function pointer contract '" + str + "' not found.");
425
426 // triggers signature compatibility checking
427 contract_handler.get_pure_contract_symbol(str);
428
429 log.status() << "Wrapping function pointer contract '" << fp_contract
430 << "' with itself in REPLACE mode" << messaget::eom;
431
432 swap_and_wrap.swap_and_wrap_replace(
433 fp_contract, fp_contract, new_contracts);
434 swapped.insert(fp_contract);
435
436 // remove it from the set of symbols to process
437 if(other_symbols.find(fp_contract) != other_symbols.end())
438 other_symbols.erase(fp_contract);
439 }
440 }
441 // process newly discovered contracts
442 function_pointer_contracts = new_contracts;
443 }
444}
445
447{
448 // instrument all other remaining functions
449 for(const auto &function_id : other_symbols)
450 {
451 // Don't instrument CPROVER and internal functions
452 if(instrument.do_not_instrument(function_id))
453 {
454 continue;
455 }
456
457 log.status() << "Instrumenting '" << function_id << "'" << messaget::eom;
458
459 instrument.instrument_function(
461 }
462
463 goto_model.goto_functions.update();
464}
465
467{
476
477 // take the max of function of loop contracts assigns clauses
478 auto assigns_clause_size = instrument.get_max_assigns_clause_size();
479 if(assigns_clause_size > max_assigns_clause_size)
480 max_assigns_clause_size = assigns_clause_size;
481
482 log.status() << "Specializing cprover_contracts functions for assigns "
483 "clauses of at most "
484 << max_assigns_clause_size << " targets" << messaget::eom;
486
487 library.inhibit_front_end_builtins();
488
489 // TODO implement a means to inhibit unreachable functions (possibly via the
490 // code that implements drop-unused-functions followed by
491 // generate-function-bodies):
492 // Traverse the call tree from the given entry point to identify
493 // functions symbols that are effectively called in the model,
494 // Then goes over all functions of the model and turns the bodies of all
495 // functions that are not in the used function set into:
496 // ```c
497 // assert(false, "function identified as unreachable");
498 // assume(false);
499 // ```
500 // That way, if the analysis mistakenly pruned some functions, assertions
501 // will be violated and the analysis will fail.
502 // TODO: add a command line flag to tell the instrumentation to not prune
503 // a function.
504 goto_model.goto_functions.update();
505
507 goto_model.goto_functions.update();
508
509 log.status() << "Removing unused functions" << messaget::eom;
510
511 // This can prune too many functions if function pointers have not been
512 // yet been removed or if the entry point is not defined.
513 // Another solution would be to rewrite the bodies of functions that seem to
514 // be unreachable into assert(false);assume(false)
516 goto_model.goto_functions.update();
517
519}
520
522{
523 // collect set of functions which are now instrumented
524 std::set<irep_idt> instrumented_functions;
525 instrument.get_instrumented_functions(instrumented_functions);
526 swap_and_wrap.get_swapped_functions(instrumented_functions);
527
528 log.status() << "Updating init function" << messaget::eom;
529 if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
532
533 // Initialize the map of instrumented functions by adding extra instructions
534 // to the harness function
535 auto &init_function = goto_model.goto_functions.function_map[harness_id];
536 auto &body = init_function.body;
537 auto begin = body.instructions.begin();
538 goto_programt payload;
539 library.add_instrumented_functions_map_init_instructions(
540 instrumented_functions, begin->source_location(), payload);
541 body.destructive_insert(begin, payload);
542
543 // Define harness as the entry point, overriding any preexisting one.
544 log.status() << "Setting entry point to " << harness_id << messaget::eom;
545 // remove the CPROVER start function
546 goto_model.symbol_table.erase(
547 goto_model.symbol_table.symbols.find(goto_functionst::entry_point()));
548 // regenerate the CPROVER start function
551 goto_model.symbol_table,
554
555 goto_model.goto_functions.update();
556}
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:305
void instrument_other_functions()
Definition dfcc.cpp:446
const loop_contract_configt loop_contract_config
Definition dfcc.h:173
void reinitialize_model()
Re-initialise the GOTO model.
Definition dfcc.cpp:521
const std::set< std::string > & to_exclude_from_nondet_static
Definition dfcc.h:174
void link_model_and_load_dfcc_library()
Definition dfcc.cpp:283
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:141
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:330
void lift_memory_predicates()
Definition dfcc.cpp:318
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:192
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:466
dfcc_instrumentt instrument
Definition dfcc.h:184
dfcc_libraryt library
Definition dfcc.h:180
void wrap_replaced_functions()
Definition dfcc.cpp:359
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:256
void wrap_discovered_function_pointer_contracts()
Definition dfcc.cpp:376
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:50
std::string what() const override
A human readable description of what went wrong.
Definition dfcc.cpp:58
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
static std::pair< irep_idt, irep_idt > parse_function_contract_pair(const irep_idt &cli_flag)
Definition dfcc.cpp:74
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.
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:113
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)
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