CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
function_call_harness_generator.cpp
Go to the documentation of this file.
1/******************************************************************\
2
3Module: harness generator for functions
4
5Author: Diffblue Ltd.
6
7\******************************************************************/
8
10
11#include <util/arith_tools.h>
12#include <util/c_types.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{
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);
71 void generate_initialisation_code_for(code_blockt &block, const exprt &lhs);
81 void call_function(
82 const code_function_callt::argumentst &arguments,
92 std::unordered_set<irep_idt>
94};
95
97 ui_message_handlert &message_handler)
99{
100 p_impl->message_handler = &message_handler;
101}
102
104
106 const std::string &option,
107 const std::list<std::string> &values)
108{
109 auto &require_exactly_one_value =
111
112 if(p_impl->recursive_initialization_config.handle_option(option, values))
113 {
114 // the option belongs to recursive initialization
115 }
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 {
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 {
190 std::transform(
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 {
202 std::transform(
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
238 auto const arguments = declare_arguments(function_body);
239
240 // configure and create recursive initialisation object
249 {
251 pair.second);
252 }
257 recursive_initialization = std::make_unique<recursive_initializationt>(
259
261 call_function(arguments, function_body);
262 for(const auto &global_pointer : global_pointers)
263 {
265 }
266 recursive_initialization->free_cluster_origins(function_body);
268}
269
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 }
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;
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 {
384 goto_model.symbol_table.lookup(nullable);
385
387 {
389 "nullable function pointer `" + id2string(nullable) +
390 "' not found in symbol table",
392 }
393
395
397 {
399 "`" + id2string(nullable) + "' is not a pointer",
401 }
402
405 {
407 "`" + id2string(nullable) + "' is not pointing to a function",
409 }
410 }
411}
412
413const 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
447 harness_function_symbol.pretty_name = harness_function_name;
448
449 harness_function_symbol.is_lvalue = true;
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
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
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());
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;
503 if(
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(
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(
527 id2string(parameter_name) + " is not a parameter");
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,
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
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) + "::";
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}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
signedbv_typet signed_int_type()
Definition c_types.cpp:22
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition ai.cpp:194
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
A codet representing sequential composition of program statements.
Definition std_code.h:130
goto_instruction_codet representation of a function call statement.
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
typet & type()
Return the type of the expression.
Definition expr.h:84
source_locationt & add_source_location()
Definition expr.h:236
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 ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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.
Symbol table entry.
Definition symbol.h:28
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...
STL namespace.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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
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::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::unordered_set< irep_idt > potential_null_function_pointers
typet remove_const(typet type)
Remove const qualifier from type (if any).
Definition type.cpp:32