CBMC
dfcc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: 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>
16 #include <util/mathematical_expr.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>
36 #include <ansi-c/cprover_library.h>
42 #include <langapi/language.h>
43 #include <langapi/language_file.h>
44 #include <langapi/mode.h>
46 
48 
51  std::string reason,
52  std::string correct_format)
53  : cprover_exception_baset(std::move(reason)),
54  correct_format(std::move(correct_format))
55 {
56 }
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 
73 static 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 
113 void 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,
143  goto_modelt &goto_model,
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,
148  const loop_contract_configt loop_contract_config,
149  message_handlert &message_handler,
150  const std::set<std::string> &to_exclude_from_nondet_static)
151  : options(options),
152  goto_model(goto_model),
153  harness_id(harness_id),
154  to_check(to_check),
155  allow_recursive_calls(allow_recursive_calls),
156  to_replace(to_replace),
157  loop_contract_config(loop_contract_config),
158  to_exclude_from_nondet_static(to_exclude_from_nondet_static),
159  message_handler(message_handler),
160  log(message_handler),
161  library(goto_model, message_handler),
162  ns(goto_model.symbol_table),
163  spec_functions(goto_model, message_handler, library),
164  contract_clauses_codegen(goto_model, message_handler, library),
165  instrument(
166  goto_model,
167  message_handler,
168  library,
169  spec_functions,
170  contract_clauses_codegen),
171  memory_predicates(goto_model, library, instrument, message_handler),
172  contract_handler(
173  goto_model,
174  message_handler,
175  library,
176  instrument,
177  memory_predicates,
178  spec_functions,
179  contract_clauses_codegen),
180  swap_and_wrap(
181  goto_model,
182  message_handler,
183  library,
184  instrument,
185  spec_functions,
186  contract_handler),
187  max_assigns_clause_size(0)
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;
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
299 
300  // add C prover lib again to fetch any dependencies of the dfcc functions
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 
314 
315  other_symbols.erase(harness_id);
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 
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 =
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;
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
428 
429  log.status() << "Wrapping function pointer contract '" << fp_contract
430  << "' with itself in REPLACE mode" << messaget::eom;
431 
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 
461  }
462 
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 
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.
505 
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)
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;
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;
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
548  // regenerate the CPROVER start function
554 
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...
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: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
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
void link_model_and_load_dfcc_library()
Definition: dfcc.cpp:283
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
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
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.
Definition: goto_program.h:73
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
mstreamt & status() const
Definition: message.h:406
mstreamt & debug() const
Definition: message.h:421
message_handlert & get_message_handler()
Definition: message.h:183
static eomt eom
Definition: message.h:289
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
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.
double log(double x)
Definition: math.c:2776
API to expression classes for 'mathematical' expressions.
Mathematical types.
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
Definition: remove_skip.cpp:87
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)
irep_idt arch
Definition: config.h:223
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.
Definition: dfcc_utils.cpp:72
static bool function_symbol_with_body_exists(const goto_modelt &, const irep_idt &function_id)
Definition: dfcc_utils.cpp:65
static bool function_symbol_exists(const goto_modelt &, const irep_idt &function_id)
Returns true iff the given symbol exists and satisfies requirements.
Definition: dfcc_utils.cpp:58
Loop contract configurations.