cprover
Loading...
Searching...
No Matches
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/make_unique.h>
15#include <util/prefix.h>
16#include <util/std_code.h>
17#include <util/string_utils.h>
18#include <util/ui_message.h>
19
23
24#include <algorithm>
25#include <iterator>
26#include <set>
27
31
35/* NOLINTNEXTLINE(readability/identifier_spacing) */
37{
43 bool nondet_globals = false;
44
46 std::unique_ptr<recursive_initializationt> recursive_initialization;
47
50
51 std::vector<std::set<irep_idt>> function_parameters_to_treat_equal;
52 std::vector<std::set<irep_idt>> function_arguments_to_treat_equal;
53
56
57 std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
58 std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
59
60 std::set<symbol_exprt> global_pointers;
61
63 void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
70 void generate_initialisation_code_for(code_blockt &block, const exprt &lhs);
80 void call_function(
81 const code_function_callt::argumentst &arguments,
91 std::unordered_set<irep_idt>
93};
94
96 ui_message_handlert &message_handler)
98{
99 p_impl->message_handler = &message_handler;
100}
101
103
105 const std::string &option,
106 const std::list<std::string> &values)
107{
108 auto &require_exactly_one_value =
110
111 if(p_impl->recursive_initialization_config.handle_option(option, values))
112 {
113 // the option belongs to recursive initialization
114 }
116 {
117 p_impl->function = require_exactly_one_value(option, values);
118 }
120 {
121 p_impl->nondet_globals = true;
122 }
124 {
125 p_impl->function_parameters_to_treat_as_arrays.insert(
126 values.begin(), values.end());
127 }
129 {
130 for(auto const &value : values)
131 {
132 for(auto const &param_cluster : split_string(value, ';'))
133 {
134 std::set<irep_idt> equal_param_set;
135 for(auto const &param_id : split_string(param_cluster, ','))
136 {
138 }
139 p_impl->function_parameters_to_treat_equal.push_back(equal_param_set);
140 }
141 }
142 }
144 {
145 for(auto const &array_size_pair : values)
146 {
147 try
148 {
149 std::string array;
150 std::string size;
151 split_string(array_size_pair, ':', array, size);
152 // --associated-array-size implies --treat-pointer-as-array
153 // but it is not an error to specify both, so we don't check
154 // for duplicates here
155 p_impl->function_parameters_to_treat_as_arrays.insert(array);
156 auto const inserted =
157 p_impl->function_parameter_to_associated_array_size.emplace(
158 array, size);
159 if(!inserted.second)
160 {
162 "can not have two associated array sizes for one array",
164 }
165 }
166 catch(const deserialization_exceptiont &)
167 {
169 "'" + array_size_pair +
170 "' is in an invalid format for array size pair",
172 "array_name:size_name, where both are the names of function "
173 "parameters"};
174 }
175 }
176 }
178 {
179 p_impl->function_parameters_to_treat_as_cstrings.insert(
180 values.begin(), values.end());
181 }
183 {
184 p_impl->recursive_initialization_config.arguments_may_be_equal = true;
185 }
187 {
188 std::transform(
189 values.begin(),
190 values.end(),
191 std::inserter(
192 p_impl->recursive_initialization_config
193 .potential_null_function_pointers,
194 p_impl->recursive_initialization_config.potential_null_function_pointers
195 .end()),
196 [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
197 }
199 {
200 std::transform(
201 values.begin(),
202 values.end(),
203 std::inserter(
204 p_impl->recursive_initialization_config
205 .potential_null_function_pointers,
206 p_impl->recursive_initialization_config.potential_null_function_pointers
207 .end()),
208 [](const std::string &opt) -> irep_idt { return irep_idt{opt}; });
209 }
210 else
211 {
213 "function harness generator cannot handle this option", "--" + option};
214 }
215}
216
218 goto_modelt &goto_model,
219 const irep_idt &harness_function_name)
220{
221 p_impl->generate(goto_model, harness_function_name);
222}
223
225 goto_modelt &goto_model,
226 const irep_idt &harness_function_name)
227{
228 symbol_table = &goto_model.symbol_table;
229 goto_functions = &goto_model.goto_functions;
230 this->harness_function_name = harness_function_name;
233
234 // create body for the function
236 auto const arguments = declare_arguments(function_body);
237
238 // configure and create recursive initialisation object
247 {
249 pair.second);
250 }
257
259 call_function(arguments, function_body);
260 for(const auto &global_pointer : global_pointers)
261 {
263 }
264 recursive_initialization->free_cluster_origins(function_body);
266}
267
270{
271 if(nondet_globals)
272 {
273 // generating initialisation code may introduce new globals
274 // i.e. modify the symbol table.
275 // Modifying the symbol table while iterating over it is not
276 // a good idea, therefore we just collect the names of globals
277 // we need to initialise first and then generate the
278 // initialisation code for all of them.
279 auto globals = std::vector<symbol_exprt>{};
280 for(const auto &symbol_table_entry : *symbol_table)
281 {
282 const auto &symbol = symbol_table_entry.second;
284 {
285 globals.push_back(symbol.symbol_expr());
286 }
287 }
288 for(auto const &global : globals)
289 {
290 generate_initialisation_code_for(function_body, global);
291 }
292 }
293}
294
296 code_blockt &block,
297 const exprt &lhs)
298{
299 recursive_initialization->initialize(
300 lhs, from_integer(0, signed_int_type()), block);
301 if(recursive_initialization->needs_freeing(lhs))
302 global_pointers.insert(to_symbol_expr(lhs));
303}
304
306 const goto_modelt &goto_model)
307{
308 if(p_impl->function == ID_empty_string)
310 "required parameter entry function not set",
312 if(
313 p_impl->recursive_initialization_config.min_dynamic_array_size >
314 p_impl->recursive_initialization_config.max_dynamic_array_size)
315 {
317 "min dynamic array size cannot be greater than max dynamic array size",
320 }
321
322 const auto function_to_call_pointer =
323 goto_model.symbol_table.lookup(p_impl->function);
324 if(function_to_call_pointer == nullptr)
325 {
327 "entry function `" + id2string(p_impl->function) +
328 "' does not exist in the symbol table",
330 }
333 for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal)
334 {
335 for(auto const &pointer_id : equal_cluster)
336 {
337 std::string decorated_pointer_id =
338 id2string(p_impl->function) + "::" + id2string(pointer_id);
339 bool is_a_param = false;
341 for(auto const &formal_param : ftype.parameters())
342 {
343 if(formal_param.get_identifier() == decorated_pointer_id)
344 {
345 is_a_param = true;
346 if(formal_param.type().id() != ID_pointer)
347 {
349 id2string(pointer_id) + " is not a pointer parameter",
351 }
352 if(common_type.id() != ID_empty)
353 {
354 if(common_type != formal_param.type())
355 {
357 "pointer arguments of conflicting type",
359 }
360 }
361 else
362 common_type = formal_param.type();
363 }
364 }
365 if(!is_a_param)
366 {
368 id2string(pointer_id) + " is not a parameter",
370 }
371 }
372 }
373
374 const namespacet ns{goto_model.symbol_table};
375
376 // Make sure all function pointers that the user asks are nullable are
377 // present in the symbol table.
378 for(const auto &nullable :
379 p_impl->recursive_initialization_config.potential_null_function_pointers)
380 {
382 goto_model.symbol_table.lookup(nullable);
383
385 {
387 "nullable function pointer `" + id2string(nullable) +
388 "' not found in symbol table",
390 }
391
392 const auto &function_pointer_type =
393 ns.follow(function_pointer_symbol_pointer->type);
394
396 {
398 "`" + id2string(nullable) + "' is not a pointer",
400 }
401
404 {
406 "`" + id2string(nullable) + "' is not pointing to a function",
408 }
409 }
410}
411
412const symbolt &
414{
415 auto function_found = symbol_table->lookup(function);
416
417 if(function_found == nullptr)
418 {
420 "function that should be harnessed is not found " + id2string(function),
422 }
423
424 return *function_found;
425}
426
429{
430 if(symbol_table->lookup(harness_function_name))
431 {
433 "harness function already exists in the symbol table",
435 }
436}
437
440{
441 const auto &function_to_call = lookup_function_to_call();
442
443 // create the function symbol
446 harness_function_symbol.pretty_name = harness_function_name;
447
448 harness_function_symbol.is_lvalue = true;
451 harness_function_symbol.value = std::move(function_body);
452
453 symbol_table->insert(harness_function_symbol);
454
455 goto_convert(*symbol_table, *goto_functions, *message_handler);
456}
457
461{
462 const auto &function_to_call = lookup_function_to_call();
463 const auto &function_type = to_code_type(function_to_call.type);
464 const auto &parameters = function_type.parameters();
465
467
468 auto allocate_objects = allocate_objectst{function_to_call.mode,
469 function_to_call.location,
470 "__goto_harness",
471 *symbol_table};
472 std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
473 for(const auto &parameter : parameters)
474 {
475 auto argument = allocate_objects.allocate_automatic_local_object(
476 remove_const(parameter.type()), parameter.get_base_name());
478 {parameter.get_base_name(), argument.get_identifier()});
479 arguments.push_back(argument);
480 }
481
482 for(const auto &pair : parameter_name_to_argument_name)
483 {
484 auto const &parameter_name = pair.first;
485 auto const &argument_name = pair.second;
486 if(function_parameters_to_treat_as_arrays.count(parameter_name) != 0)
487 {
488 function_arguments_to_treat_as_arrays.insert(argument_name);
489 }
490
491 if(function_parameters_to_treat_as_cstrings.count(parameter_name) != 0)
492 {
493 function_arguments_to_treat_as_cstrings.insert(argument_name);
494 }
495
496 auto it = function_parameter_to_associated_array_size.find(parameter_name);
497 if(it != function_parameter_to_associated_array_size.end())
498 {
499 auto const &associated_array_size_parameter = it->second;
502 if(
504 {
506 "could not find parameter to associate the array size of array \"" +
507 id2string(parameter_name) + "\" (Expected parameter: \"" +
508 id2string(associated_array_size_parameter) + "\" on function \"" +
509 id2string(function_to_call.display_name()) + "\" in " +
510 function_to_call.location.as_string() + ")",
512 }
513 function_argument_to_associated_array_size.insert(
515 }
516 }
517
518 // translate the parameter to argument also in the equality clusters
519 for(auto const &equal_cluster : function_parameters_to_treat_equal)
520 {
521 std::set<irep_idt> cluster_argument_names;
522 for(auto const &parameter_name : equal_cluster)
523 {
524 INVARIANT(
526 id2string(parameter_name) + " is not a parameter");
529 }
530 function_arguments_to_treat_equal.push_back(cluster_argument_names);
531 }
532
533 allocate_objects.declare_created_symbols(function_body);
534 return arguments;
535}
536
538 const code_function_callt::argumentst &arguments,
540{
541 auto const &function_to_call = lookup_function_to_call();
542 for(auto const &argument : arguments)
543 {
544 generate_initialisation_code_for(function_body, argument);
545 if(recursive_initialization->needs_freeing(argument))
546 global_pointers.insert(to_symbol_expr(argument));
547 }
548 code_function_callt function_call{function_to_call.symbol_expr(),
549 std::move(arguments)};
550 function_call.add_source_location() = function_to_call.location;
551
552 function_body.add(std::move(function_call));
553}
554
557{
558 std::unordered_set<irep_idt> nullables;
559 for(const auto &nullable :
560 recursive_initialization_config.potential_null_function_pointers)
561 {
562 const auto &nullable_name = id2string(nullable);
563 const auto &function_prefix = id2string(function) + "::";
565 {
566 nullables.insert(
567 "__goto_harness::" + nullable_name.substr(function_prefix.size()));
568 }
569 else
570 {
571 nullables.insert(nullable_name);
572 }
573 }
574 return nullables;
575}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void base_type(typet &type, const namespacet &ns)
signedbv_typet signed_int_type()
Definition c_types.cpp:40
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:189
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
A codet representing sequential composition of program statements.
Definition std_code.h:130
codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
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:37
The empty type.
Definition std_types.h:51
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
source_locationt & add_source_location()
Definition expr.h:235
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:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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_tablet &symbol_table, const irep_idt &id, const irep_idt &argument)
Definition function.cpp:25
#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:47
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
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...
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:189
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
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