CBMC
function_call_harness_generator.cpp
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: harness generator for functions
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
10 
11 #include <util/arith_tools.h>
12 #include <util/c_types.h>
13 #include <util/exception_utils.h>
14 #include <util/prefix.h>
15 #include <util/std_code.h>
16 #include <util/string_utils.h>
17 #include <util/ui_message.h>
18 
20 
23 
27 
28 #include <algorithm>
29 #include <iterator>
30 #include <set>
31 #include <utility>
32 
36 /* NOLINTNEXTLINE(readability/identifier_spacing) */
38 {
40  irep_idt function;
44  bool nondet_globals = false;
45 
47  std::unique_ptr<recursive_initializationt> recursive_initialization;
48 
51 
52  std::vector<std::set<irep_idt>> function_parameters_to_treat_equal;
53  std::vector<std::set<irep_idt>> function_arguments_to_treat_equal;
54 
57 
58  std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
59  std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
60 
61  std::set<symbol_exprt> global_pointers;
62 
64  void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
67  void generate_nondet_globals(code_blockt &function_body);
71  void generate_initialisation_code_for(code_blockt &block, const exprt &lhs);
81  void call_function(
82  const code_function_callt::argumentst &arguments,
83  code_blockt &function_body);
92  std::unordered_set<irep_idt>
94 };
95 
97  ui_message_handlert &message_handler)
98  : goto_harness_generatort{}, p_impl(std::make_unique<implt>())
99 {
100  p_impl->message_handler = &message_handler;
101 }
102 
104 
106  const std::string &option,
107  const std::list<std::string> &values)
108 {
111 
112  if(p_impl->recursive_initialization_config.handle_option(option, values))
113  {
114  // the option belongs to recursive initialization
115  }
116  else if(option == FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT)
117  {
118  p_impl->function = require_exactly_one_value(option, values);
119  }
121  {
122  p_impl->nondet_globals = true;
123  }
125  {
126  p_impl->function_parameters_to_treat_as_arrays.insert(
127  values.begin(), values.end());
128  }
130  {
131  for(auto const &value : values)
132  {
133  for(auto const &param_cluster : split_string(value, ';'))
134  {
135  std::set<irep_idt> equal_param_set;
136  for(auto const &param_id : split_string(param_cluster, ','))
137  {
138  equal_param_set.insert(param_id);
139  }
140  p_impl->function_parameters_to_treat_equal.push_back(
141  std::move(equal_param_set));
142  }
143  }
144  }
146  {
147  for(auto const &array_size_pair : values)
148  {
149  try
150  {
151  std::string array;
152  std::string size;
153  split_string(array_size_pair, ':', array, size);
154  // --associated-array-size implies --treat-pointer-as-array
155  // but it is not an error to specify both, so we don't check
156  // for duplicates here
157  p_impl->function_parameters_to_treat_as_arrays.insert(array);
158  auto const inserted =
159  p_impl->function_parameter_to_associated_array_size.emplace(
160  array, size);
161  if(!inserted.second)
162  {
164  "can not have two associated array sizes for one array",
166  }
167  }
168  catch(const deserialization_exceptiont &)
169  {
171  "'" + array_size_pair +
172  "' is in an invalid format for array size pair",
174  "array_name:size_name, where both are the names of function "
175  "parameters"};
176  }
177  }
178  }
180  {
181  p_impl->function_parameters_to_treat_as_cstrings.insert(
182  values.begin(), values.end());
183  }
185  {
186  p_impl->recursive_initialization_config.arguments_may_be_equal = true;
187  }
189  {
191  values.begin(),
192  values.end(),
193  std::inserter(
194  p_impl->recursive_initialization_config
195  .potential_null_function_pointers,
196  p_impl->recursive_initialization_config.potential_null_function_pointers
197  .end()),
198  [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
199  }
201  {
203  values.begin(),
204  values.end(),
205  std::inserter(
206  p_impl->recursive_initialization_config
207  .potential_null_function_pointers,
208  p_impl->recursive_initialization_config.potential_null_function_pointers
209  .end()),
210  [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
211  }
212  else
213  {
215  "function harness generator cannot handle this option", "--" + option};
216  }
217 }
218 
220  goto_modelt &goto_model,
221  const irep_idt &harness_function_name)
222 {
223  p_impl->generate(goto_model, harness_function_name);
224 }
225 
227  goto_modelt &goto_model,
228  const irep_idt &harness_function_name)
229 {
230  symbol_table = &goto_model.symbol_table;
231  goto_functions = &goto_model.goto_functions;
232  this->harness_function_name = harness_function_name;
235 
236  // create body for the function
237  code_blockt function_body{};
238  auto const arguments = declare_arguments(function_body);
239 
240  // configure and create recursive initialisation object
248  for(const auto &pair : function_argument_to_associated_array_size)
249  {
251  pair.second);
252  }
257  recursive_initialization = std::make_unique<recursive_initializationt>(
258  recursive_initialization_config, goto_model);
259 
260  generate_nondet_globals(function_body);
261  call_function(arguments, function_body);
262  for(const auto &global_pointer : global_pointers)
263  {
264  recursive_initialization->free_if_possible(global_pointer, function_body);
265  }
266  recursive_initialization->free_cluster_origins(function_body);
267  add_harness_function_to_goto_model(std::move(function_body));
268 }
269 
271  code_blockt &function_body)
272 {
273  if(nondet_globals)
274  {
275  // generating initialisation code may introduce new globals
276  // i.e. modify the symbol table.
277  // Modifying the symbol table while iterating over it is not
278  // a good idea, therefore we just collect the names of globals
279  // we need to initialise first and then generate the
280  // initialisation code for all of them.
281  auto globals = std::vector<symbol_exprt>{};
282  for(const auto &symbol_table_entry : *symbol_table)
283  {
284  const auto &symbol = symbol_table_entry.second;
286  {
287  globals.push_back(symbol.symbol_expr());
288  }
289  }
290  for(auto const &global : globals)
291  {
292  generate_initialisation_code_for(function_body, global);
293  }
294  }
295 }
296 
298  code_blockt &block,
299  const exprt &lhs)
300 {
301  recursive_initialization->initialize(
302  lhs, from_integer(0, signed_int_type()), block);
303  if(recursive_initialization->needs_freeing(lhs))
304  global_pointers.insert(to_symbol_expr(lhs));
305 }
306 
308  const goto_modelt &goto_model)
309 {
310  if(p_impl->function == ID_empty_string)
312  "required parameter entry function not set",
314  if(
315  p_impl->recursive_initialization_config.min_dynamic_array_size >
316  p_impl->recursive_initialization_config.max_dynamic_array_size)
317  {
319  "min dynamic array size cannot be greater than max dynamic array size",
322  }
323 
324  const auto function_to_call_pointer =
325  goto_model.symbol_table.lookup(p_impl->function);
326  if(function_to_call_pointer == nullptr)
327  {
329  "entry function `" + id2string(p_impl->function) +
330  "' does not exist in the symbol table",
332  }
333  const auto &function_to_call = *function_to_call_pointer;
334  const auto &ftype = to_code_type(function_to_call.type);
335  for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal)
336  {
337  for(auto const &pointer_id : equal_cluster)
338  {
339  std::string decorated_pointer_id =
340  id2string(p_impl->function) + "::" + id2string(pointer_id);
341  bool is_a_param = false;
342  typet common_type = empty_typet{};
343  for(auto const &formal_param : ftype.parameters())
344  {
345  if(formal_param.get_identifier() == decorated_pointer_id)
346  {
347  is_a_param = true;
348  if(formal_param.type().id() != ID_pointer)
349  {
351  id2string(pointer_id) + " is not a pointer parameter",
353  }
354  if(common_type.id() != ID_empty)
355  {
356  if(common_type != formal_param.type())
357  {
359  "pointer arguments of conflicting type",
361  }
362  }
363  else
364  common_type = formal_param.type();
365  }
366  }
367  if(!is_a_param)
368  {
370  id2string(pointer_id) + " is not a parameter",
372  }
373  }
374  }
375 
376  const namespacet ns{goto_model.symbol_table};
377 
378  // Make sure all function pointers that the user asks are nullable are
379  // present in the symbol table.
380  for(const auto &nullable :
381  p_impl->recursive_initialization_config.potential_null_function_pointers)
382  {
383  const auto &function_pointer_symbol_pointer =
384  goto_model.symbol_table.lookup(nullable);
385 
386  if(function_pointer_symbol_pointer == nullptr)
387  {
389  "nullable function pointer `" + id2string(nullable) +
390  "' not found in symbol table",
392  }
393 
394  const auto &function_pointer_type = function_pointer_symbol_pointer->type;
395 
396  if(!can_cast_type<pointer_typet>(function_pointer_type))
397  {
399  "`" + id2string(nullable) + "' is not a pointer",
401  }
402 
404  to_pointer_type(function_pointer_type).base_type()))
405  {
407  "`" + id2string(nullable) + "' is not pointing to a function",
409  }
410  }
411 }
412 
413 const symbolt &
415 {
416  auto function_found = symbol_table->lookup(function);
417 
418  if(function_found == nullptr)
419  {
421  "function that should be harnessed is not found " + id2string(function),
423  }
424 
425  return *function_found;
426 }
427 
430 {
431  if(symbol_table->lookup(harness_function_name))
432  {
434  "harness function already exists in the symbol table",
436  }
437 }
438 
441 {
442  const auto &function_to_call = lookup_function_to_call();
443 
444  // create the function symbol
445  symbolt harness_function_symbol{};
446  harness_function_symbol.name = harness_function_symbol.base_name =
447  harness_function_symbol.pretty_name = harness_function_name;
448 
449  harness_function_symbol.is_lvalue = true;
450  harness_function_symbol.mode = function_to_call.mode;
451  harness_function_symbol.type = code_typet{{}, empty_typet{}};
452  harness_function_symbol.value = std::move(function_body);
453 
454  symbol_table->insert(harness_function_symbol);
455 
456  goto_convert(*symbol_table, *goto_functions, *message_handler);
457 }
458 
461  code_blockt &function_body)
462 {
463  const auto &function_to_call = lookup_function_to_call();
464  const auto &function_type = to_code_type(function_to_call.type);
465  const auto &parameters = function_type.parameters();
466 
467  code_function_callt::operandst arguments{};
468 
469  auto allocate_objects = allocate_objectst{function_to_call.mode,
470  function_to_call.location,
471  "__goto_harness",
472  *symbol_table};
473  std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
474  for(const auto &parameter : parameters)
475  {
476  auto argument = allocate_objects.allocate_automatic_local_object(
477  remove_const(parameter.type()), parameter.get_base_name());
478  parameter_name_to_argument_name.insert(
479  {parameter.get_base_name(), argument.get_identifier()});
480  arguments.push_back(argument);
481  }
482 
483  for(const auto &pair : parameter_name_to_argument_name)
484  {
485  auto const &parameter_name = pair.first;
486  auto const &argument_name = pair.second;
487  if(function_parameters_to_treat_as_arrays.count(parameter_name) != 0)
488  {
489  function_arguments_to_treat_as_arrays.insert(argument_name);
490  }
491 
492  if(function_parameters_to_treat_as_cstrings.count(parameter_name) != 0)
493  {
494  function_arguments_to_treat_as_cstrings.insert(argument_name);
495  }
496 
497  auto it = function_parameter_to_associated_array_size.find(parameter_name);
498  if(it != function_parameter_to_associated_array_size.end())
499  {
500  auto const &associated_array_size_parameter = it->second;
501  auto associated_array_size_argument =
502  parameter_name_to_argument_name.find(associated_array_size_parameter);
503  if(
504  associated_array_size_argument == parameter_name_to_argument_name.end())
505  {
507  "could not find parameter to associate the array size of array \"" +
508  id2string(parameter_name) + "\" (Expected parameter: \"" +
509  id2string(associated_array_size_parameter) + "\" on function \"" +
510  id2string(function_to_call.display_name()) + "\" in " +
511  function_to_call.location.as_string() + ")",
513  }
514  function_argument_to_associated_array_size.insert(
515  {argument_name, associated_array_size_argument->second});
516  }
517  }
518 
519  // translate the parameter to argument also in the equality clusters
520  for(auto const &equal_cluster : function_parameters_to_treat_equal)
521  {
522  std::set<irep_idt> cluster_argument_names;
523  for(auto const &parameter_name : equal_cluster)
524  {
525  INVARIANT(
526  parameter_name_to_argument_name.count(parameter_name) != 0,
527  id2string(parameter_name) + " is not a parameter");
528  cluster_argument_names.insert(
529  parameter_name_to_argument_name[parameter_name]);
530  }
531  function_arguments_to_treat_equal.push_back(
532  std::move(cluster_argument_names));
533  }
534 
535  allocate_objects.declare_created_symbols(function_body);
536  return arguments;
537 }
538 
540  const code_function_callt::argumentst &arguments,
541  code_blockt &function_body)
542 {
543  auto const &function_to_call = lookup_function_to_call();
544  for(auto const &argument : arguments)
545  {
546  generate_initialisation_code_for(function_body, argument);
547  if(recursive_initialization->needs_freeing(argument))
548  global_pointers.insert(to_symbol_expr(argument));
549  }
550  code_function_callt function_call{function_to_call.symbol_expr(),
551  std::move(arguments)};
552  function_call.add_source_location() = function_to_call.location;
553 
554  function_body.add(std::move(function_call));
555 }
556 
557 std::unordered_set<irep_idt> function_call_harness_generatort::implt::
559 {
560  std::unordered_set<irep_idt> nullables;
561  for(const auto &nullable :
562  recursive_initialization_config.potential_null_function_pointers)
563  {
564  const auto &nullable_name = id2string(nullable);
565  const auto &function_prefix = id2string(function) + "::";
566  if(has_prefix(nullable_name, function_prefix))
567  {
568  nullables.insert(
569  "__goto_harness::" + nullable_name.substr(function_prefix.size()));
570  }
571  else
572  {
573  nullables.insert(nullable_name);
574  }
575  }
576  return nullables;
577 }
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
signedbv_typet signed_int_type()
Definition: c_types.cpp:22
unsigned char opt
Definition: cegis.c:20
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
Base type of functions.
Definition: std_types.h:583
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
The empty type.
Definition: std_types.h:51
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
source_locationt & add_source_location()
Definition: expr.h:236
typet & type()
Return the type of the expression.
Definition: expr.h:84
void validate_options(const goto_modelt &goto_model) override
Check if options are in a sane state, throw otherwise.
function_call_harness_generatort(ui_message_handlert &message_handler)
void handle_option(const std::string &option, const std::list< std::string > &values) override
Handle a command line argument.
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
Generate a harness according to the set options.
A collection of goto functions.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & id() const
Definition: irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
static bool is_initialization_allowed(const symbolt &symbol)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt name
The unique identifier.
Definition: symbol.h:40
The type of an expression, extends irept.
Definition: type.h:29
#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT
#define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
#define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
code_function_callt function_to_call(symbol_table_baset &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition: function.cpp:22
#define FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT
#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_MAYBE_OPT
#define FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
#define GOTO_HARNESS_GENERATOR_HARNESS_FUNCTION_NAME_OPT
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string require_exactly_one_value(const std::string &option, const std::list< std::string > &values)
Returns the only value of a single element list, throws an exception if not passed a single element l...
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:80
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
bool can_cast_type< code_typet >(const typet &type)
Check whether a reference to a typet is a code_typet.
Definition: std_types.h:775
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
This contains implementation details of function call harness generator to avoid leaking them out int...
std::map< irep_idt, irep_idt > function_parameter_to_associated_array_size
void call_function(const code_function_callt::argumentst &arguments, code_blockt &function_body)
Write initialisation code for each of the arguments into function_body, then insert a call to the ent...
std::map< irep_idt, irep_idt > function_argument_to_associated_array_size
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
std::vector< std::set< irep_idt > > function_arguments_to_treat_equal
const symbolt & lookup_function_to_call()
Return a reference to the entry function or throw if it doesn't exist.
code_function_callt::argumentst declare_arguments(code_blockt &function_body)
Declare local variables for each of the parameters of the entry function and return them.
void add_harness_function_to_goto_model(code_blockt function_body)
Update the goto-model with the new harness function.
std::unique_ptr< recursive_initializationt > recursive_initialization
void generate_nondet_globals(code_blockt &function_body)
Iterate over the symbol table and generate initialisation code for globals into the function body.
recursive_initialization_configt recursive_initialization_config
void generate_initialisation_code_for(code_blockt &block, const exprt &lhs)
Generate initialisation code for one lvalue inside block.
std::vector< std::set< irep_idt > > function_parameters_to_treat_equal
std::unordered_set< irep_idt > map_function_parameters_to_function_argument_names()
For function parameters that are pointers to functions we want to be able to specify whether or not t...
void ensure_harness_does_not_already_exist()
Throw if the harness function already exists in the symbol table.
std::set< irep_idt > pointers_to_treat_as_cstrings
std::vector< std::set< irep_idt > > pointers_to_treat_equal
std::map< irep_idt, irep_idt > array_name_to_associated_array_size_variable
std::set< irep_idt > variables_that_hold_array_sizes
std::set< irep_idt > pointers_to_treat_as_arrays
std::unordered_set< irep_idt > potential_null_function_pointers
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition: type.cpp:32