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/optional.h>
20#include <util/pointer_expr.h>
23#include <util/prefix.h>
24#include <util/std_expr.h>
25#include <util/string_utils.h>
26
35
37#include <ansi-c/c_expr.h>
43#include <langapi/language.h>
45#include <langapi/mode.h>
47
49
52 std::string reason,
53 std::string correct_format)
54 : cprover_exception_baset(std::move(reason)),
55 correct_format(std::move(correct_format))
56{
57}
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
74#include <iostream>
75
76static std::pair<irep_idt, irep_idt>
78{
79 auto const correct_format_message =
80 "the format for function and contract pairs is "
81 "`<function_name>[/<contract_name>]`";
82
83 std::string cli_flag_str = id2string(cli_flag);
84
85 auto split = split_string(cli_flag_str, '/', true, false);
86
87 if(split.size() == 1)
88 {
89 return std::make_pair(cli_flag, cli_flag);
90 }
91 else if(split.size() == 2)
92 {
93 auto function_name = split[0];
94 if(function_name.empty())
95 {
97 "couldn't find function name before '/' in '" + cli_flag_str + "'",
99 }
100 auto contract_name = split[1];
101 if(contract_name.empty())
102 {
104 "couldn't find contract name after '/' in '" + cli_flag_str + "'",
106 }
107 return std::make_pair(function_name, contract_name);
108 }
109 else
110 {
112 "couldn't parse '" + cli_flag_str + "'", correct_format_message};
113 }
114}
115
116void dfcc(
117 const optionst &options,
118 goto_modelt &goto_model,
119 const irep_idt &harness_id,
120 const optionalt<irep_idt> &to_check,
121 const bool allow_recursive_calls,
122 const std::set<irep_idt> &to_replace,
123 const bool apply_loop_contracts,
124 const bool unwind_transformed_loops,
125 const std::set<std::string> &to_exclude_from_nondet_static,
126 message_handlert &message_handler)
127{
128 std::map<irep_idt, irep_idt> to_replace_map;
129 for(const auto &cli_flag : to_replace)
131
132 dfcc(
133 options,
134 goto_model,
135 harness_id,
136 to_check.has_value() ? parse_function_contract_pair(to_check.value())
138 allow_recursive_calls,
140 apply_loop_contracts,
141 unwind_transformed_loops,
142 to_exclude_from_nondet_static,
143 message_handler);
144}
145
146void dfcc(
147 const optionst &options,
148 goto_modelt &goto_model,
149 const irep_idt &harness_id,
150 const optionalt<std::pair<irep_idt, irep_idt>> &to_check,
151 const bool allow_recursive_calls,
152 const std::map<irep_idt, irep_idt> &to_replace,
153 const bool apply_loop_contracts,
154 const bool unwind_transformed_loops,
155 const std::set<std::string> &to_exclude_from_nondet_static,
156 message_handlert &message_handler)
157{
158 dfcct{
159 options,
160 goto_model,
161 harness_id,
162 to_check,
163 allow_recursive_calls,
164 to_replace,
166 apply_loop_contracts, unwind_transformed_loops),
167 message_handler,
168 to_exclude_from_nondet_static};
169}
170
172 const optionst &options,
173 goto_modelt &goto_model,
174 const irep_idt &harness_id,
175 const optionalt<std::pair<irep_idt, irep_idt>> &to_check,
176 const bool allow_recursive_calls,
177 const std::map<irep_idt, irep_idt> &to_replace,
178 const dfcc_loop_contract_modet loop_contract_mode,
179 message_handlert &message_handler,
180 const std::set<std::string> &to_exclude_from_nondet_static)
181 : options(options),
182 goto_model(goto_model),
183 harness_id(harness_id),
184 to_check(to_check),
185 allow_recursive_calls(allow_recursive_calls),
186 to_replace(to_replace),
187 loop_contract_mode(loop_contract_mode),
188 to_exclude_from_nondet_static(to_exclude_from_nondet_static),
189 message_handler(message_handler),
190 log(message_handler),
191 library(goto_model, message_handler),
192 ns(goto_model.symbol_table),
193 spec_functions(goto_model, message_handler, library),
194 contract_clauses_codegen(goto_model, message_handler, library),
195 instrument(
196 goto_model,
197 message_handler,
198 library,
199 spec_functions,
200 contract_clauses_codegen),
201 memory_predicates(goto_model, library, instrument, message_handler),
202 contract_handler(
203 goto_model,
204 message_handler,
205 library,
206 instrument,
207 memory_predicates,
208 spec_functions,
209 contract_clauses_codegen),
210 swap_and_wrap(
211 goto_model,
212 message_handler,
213 library,
214 instrument,
215 spec_functions,
216 contract_handler),
217 max_assigns_clause_size(0)
218{
220}
221
223{
224 // check that harness function exists
227 "Harness function '" + id2string(harness_id) +
228 "' either not found or has no body");
229
230 if(to_check.has_value())
231 {
232 auto pair = to_check.value();
235 "Function to check '" + id2string(pair.first) +
236 "' either not found or has no body");
237
238 // triggers signature compatibility checking
240
242 pair.first != harness_id,
243 "Function '" + id2string(pair.first) +
244 "' cannot be both be checked against a contract and be the harness");
245
247 pair.second != harness_id,
248 "Function '" + id2string(pair.first) +
249 "' cannot be both the contract to check and be the harness");
250
252 to_replace.find(pair.first) == to_replace.end(),
253 "Function '" + id2string(pair.first) +
254 "' cannot be both checked against contract and replaced by a contract");
255
258 "CPROVER function or builtin '" + id2string(pair.first) +
259 "' cannot be checked against a contract");
260 }
261
262 for(const auto &pair : to_replace)
263 {
264 // for functions to replace with contracts we don't require the replaced
265 // function to have a body because only the contract is actually used
268 "Function to replace '" + id2string(pair.first) + "' not found");
269
270 // triggers signature compatibility checking
272
274 pair.first != harness_id,
275 "Function '" + id2string(pair.first) +
276 "' cannot both be replaced with a contract and be the harness");
277
279 pair.second != harness_id,
280 "Function '" + id2string(pair.first) +
281 "' cannot both be the contract to use for replacement and be the "
282 "harness");
283 }
284}
285
287 std::set<irep_idt> &contract_symbols,
288 std::set<irep_idt> &other_symbols)
289{
290 // collect contract and other symbols
291 for(auto &entry : goto_model.symbol_table)
292 {
293 const symbolt &symbol = entry.second;
294
295 // not a function symbol
296 if(symbol.type.id() != ID_code)
297 continue;
298
299 // is it a pure contract ?
300 const irep_idt &sym_name = symbol.name;
301 if(symbol.is_property && has_prefix(id2string(sym_name), "contract::"))
302 {
304 }
305 else
306 {
307 // it is not a contract
308 other_symbols.insert(sym_name);
309 }
310 }
311}
312
314{
315 // load the cprover library to make sure the model is complete
316 log.status() << "Loading CPROVER C library (" << config.ansi_c.arch << ")"
317 << messaget::eom;
320
321 // this must be done before loading the dfcc lib
323
324 // load the dfcc library before instrumentation starts
326
327 // disable checks on all library functions
329
330 // add C prover lib again to fetch any dependencies of the dfcc functions
333}
334
336{
337 // instrument the harness function
338 // load the cprover library to make sure the model is complete
339 log.status() << "Instrumenting harness function '" << harness_id << "'"
340 << messaget::eom;
341
344
346}
347
349{
350 std::set<irep_idt> predicates =
352 for(const auto &predicate : predicates)
353 {
354 log.debug() << "Memory predicate" << predicate << messaget::eom;
355 if(other_symbols.find(predicate) != other_symbols.end())
356 other_symbols.erase(predicate);
357 }
358}
359
361{
362 // swap-and-wrap checked functions with contracts
363 if(to_check.has_value())
364 {
365 const auto &pair = to_check.value();
366 const auto &wrapper_id = pair.first;
367 const auto &contract_id = pair.second;
368 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
369 << contract_id << "' in CHECK mode" << messaget::eom;
370
377
378 if(other_symbols.find(wrapper_id) != other_symbols.end())
380
381 // update max contract size
382 const std::size_t assigns_clause_size =
386 }
387}
388
390{
391 // swap-and-wrap replaced functions with contracts
392 for(const auto &pair : to_replace)
393 {
394 const auto &wrapper_id = pair.first;
395 const auto &contract_id = pair.second;
396 log.status() << "Wrapping '" << wrapper_id << "' with contract '"
397 << contract_id << "' in REPLACE mode" << messaget::eom;
400
401 if(other_symbols.find(wrapper_id) != other_symbols.end())
403 }
404}
405
407{
408 std::set<irep_idt> swapped;
409 while(!function_pointer_contracts.empty())
410 {
411 std::set<irep_idt> new_contracts;
412 // swap-and-wrap function pointer contracts with themselves
413 for(const auto &fp_contract : function_pointer_contracts)
414 {
415 if(swapped.find(fp_contract) != swapped.end())
416 continue;
417
418 // contracts for function pointers must be replaced with themselves
419 // so we need to check that:
420 // - the symbol exists as a function symbol
421 // - the symbol exists as a pure contract symbol
422 // - the function symbol is not already swapped for contract checking
423 // - the function symbol is not already swapped with another contract for
424 // replacement
425
426 const auto str = id2string(fp_contract);
427
428 // Is it already swapped with another function for contract checking ?
430 !to_check.has_value() || to_check.value().first != str,
431 "Function '" + str +
432 "' used as contract for function pointer cannot be itself the object "
433 "of a contract check.");
434
435 // Is it already swapped with another function for contract checking ?
436 auto found = to_replace.find(str);
437 if(found != to_replace.end())
438 {
440 found->first == found->second,
441 "Function '" + str +
442 "' used as contract for function pointer already the object of a "
443 "contract replacement with '" +
444 id2string(found->second) + "'");
445 log.status() << "Function pointer contract '" << fp_contract
446 << "' already wrapped with itself in REPLACE mode"
447 << messaget::eom;
448 }
449 else
450 {
451 // we need to swap it with itself
454 "Function pointer contract '" + str + "' not found.");
455
456 // triggers signature compatibility checking
458
459 log.status() << "Wrapping function pointer contract '" << fp_contract
460 << "' with itself in REPLACE mode" << messaget::eom;
461
464 swapped.insert(fp_contract);
465
466 // remove it from the set of symbols to process
467 if(other_symbols.find(fp_contract) != other_symbols.end())
469 }
470 }
471 // process newly discovered contracts
473 }
474}
475
477{
478 // instrument all other remaining functions
479 for(const auto &function_id : other_symbols)
480 {
481 // Don't instrument CPROVER and internal functions
482 if(instrument.do_not_instrument(function_id))
483 {
484 continue;
485 }
486
487 log.status() << "Instrumenting '" << function_id << "'" << messaget::eom;
488
491 }
492
494}
495
497{
506
507 // take the max of function of loop contracts assigns clauses
511
512 log.status() << "Specializing cprover_contracts functions for assigns "
513 "clauses of at most "
514 << max_assigns_clause_size << " targets" << messaget::eom;
516
518
519 // TODO implement a means to inhibit unreachable functions (possibly via the
520 // code that implements drop-unused-functions followed by
521 // generate-function-bodies):
522 // Traverse the call tree from the given entry point to identify
523 // functions symbols that are effectively called in the model,
524 // Then goes over all functions of the model and turns the bodies of all
525 // functions that are not in the used function set into:
526 // ```c
527 // assert(false, "function identified as unreachable");
528 // assume(false);
529 // ```
530 // That way, if the analysis mistakenly pruned some functions, assertions
531 // will be violated and the analysis will fail.
532 // TODO: add a command line flag to tell the instrumentation to not prune
533 // a function.
535
538
539 log.status() << "Removing unused functions" << messaget::eom;
540
541 // This can prune too many functions if function pointers have not been
542 // yet been removed or if the entry point is not defined.
543 // Another solution would be to rewrite the bodies of functions that seem to
544 // be unreachable into assert(false);assume(false)
547
549}
550
552{
553 // collect set of functions which are now instrumented
554 std::set<irep_idt> instrumented_functions;
557
558 log.status() << "Updating init function" << messaget::eom;
562
563 // Initialize the map of instrumented functions by adding extra instructions
564 // to the harness function
566 auto &body = init_function.body;
567 auto begin = body.instructions.begin();
570 instrumented_functions, begin->source_location(), payload);
571 body.destructive_insert(begin, payload);
572
573 // Define harness as the entry point, overriding any preexisting one.
574 log.status() << "Setting entry point to " << harness_id << messaget::eom;
575 // remove the CPROVER start function
578 // regenerate the CPROVER start function
584
586}
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...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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 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.
const symbolt & get_pure_contract_symbol(const irep_idt &contract_id, const optionalt< irep_idt > function_id_opt={})
Searches for a symbol named "contract::contract_id" in the symbol table.
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
void instrument_harness_function(const irep_idt &function_id, const dfcc_loop_contract_modet loop_contract_mode, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function used as a proof harness.
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_function(const irep_idt &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 instrumenting its body instruc...
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 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)
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:153
goto_modelt & goto_model
Definition dfcc.h:205
std::set< irep_idt > function_pointer_contracts
Definition dfcc.h:233
const optionst & options
Definition dfcc.h:204
std::set< irep_idt > pure_contract_symbols
Definition dfcc.h:231
void instrument_harness_function()
Definition dfcc.cpp:335
void instrument_other_functions()
Definition dfcc.cpp:476
void reinitialize_model()
Re-initialise the GOTO model.
Definition dfcc.cpp:551
const std::set< std::string > & to_exclude_from_nondet_static
Definition dfcc.h:211
void link_model_and_load_dfcc_library()
Definition dfcc.cpp:313
dfcc_swap_and_wrapt swap_and_wrap
Definition dfcc.h:224
dfcc_lift_memory_predicatest memory_predicates
Definition dfcc.h:222
dfcct(const optionst &options, goto_modelt &goto_model, const irep_idt &harness_id, const optionalt< std::pair< irep_idt, irep_idt > > &to_check, const bool allow_recursive_calls, const std::map< irep_idt, irep_idt > &to_replace, const dfcc_loop_contract_modet loop_contract_mode, message_handlert &message_handler, const std::set< std::string > &to_exclude_from_nondet_static)
Class constructor.
Definition dfcc.cpp:171
void wrap_checked_function()
Definition dfcc.cpp:360
void lift_memory_predicates()
Definition dfcc.cpp:348
messaget log
Definition dfcc.h:213
const dfcc_loop_contract_modet loop_contract_mode
Definition dfcc.h:210
const optionalt< std::pair< irep_idt, irep_idt > > & to_check
Definition dfcc.h:207
void check_transform_goto_model_preconditions()
Checks preconditions on arguments of transform_goto_model.
Definition dfcc.cpp:222
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:228
void transform_goto_model()
Applies function contracts and loop contracts transformation to GOTO model using the dynamic frame co...
Definition dfcc.cpp:496
dfcc_instrumentt instrument
Definition dfcc.h:221
dfcc_libraryt library
Definition dfcc.h:217
void wrap_replaced_functions()
Definition dfcc.cpp:389
message_handlert & message_handler
Definition dfcc.h:212
const irep_idt & harness_id
Definition dfcc.h:206
const bool allow_recursive_calls
Definition dfcc.h:208
std::set< irep_idt > other_symbols
Definition dfcc.h:232
dfcc_contract_handlert contract_handler
Definition dfcc.h:223
const std::map< irep_idt, irep_idt > & to_replace
Definition dfcc.h:209
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:286
void wrap_discovered_function_pointer_contracts()
Definition dfcc.cpp:406
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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:74
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:396
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
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_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:77
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,...
dfcc_loop_contract_modet dfcc_loop_contract_mode_from_bools(bool apply_loop_contracts, bool unwind_transformed_loops)
Generates an enum value from boolean flags for application and unwinding.
dfcc_loop_contract_modet
Enumeration representing the instrumentation mode for loop contracts.
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 optionalt< irep_idt > &to_check, const bool allow_recursive_calls, const std::set< irep_idt > &to_replace, const bool apply_loop_contracts, const bool unwind_transformed_loops, 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:116
Initialize a Goto Program.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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_functionst &goto_functions, 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...
nonstd::optional< T > optionalt
Definition optional.h:35
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.