cprover
Loading...
Searching...
No Matches
generate_function_bodies.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Replace bodies of goto functions
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
10
12
17
18#include <util/fresh_symbol.h>
19#include <util/make_unique.h>
20#include <util/pointer_expr.h>
21#include <util/prefix.h>
22#include <util/string2int.h>
23#include <util/string_utils.h>
24
26 goto_functiont &function,
27 symbol_tablet &symbol_table,
28 const irep_idt &function_name) const
29{
30 PRECONDITION(!function.body_available());
31 generate_parameter_names(function, symbol_table, function_name);
32 generate_function_body_impl(function, symbol_table, function_name);
33}
34
36 goto_functiont &function,
37 symbol_tablet &symbol_table,
38 const irep_idt &function_name) const
39{
40 auto &function_symbol = symbol_table.get_writeable_ref(function_name);
41 auto &parameters = to_code_type(function_symbol.type).parameters();
42
43 int param_counter = 0;
44 for(auto &parameter : parameters)
45 {
46 if(parameter.get_identifier().empty())
47 {
48 const std::string param_base_name =
49 parameter.get_base_name().empty()
50 ? "__param$" + std::to_string(param_counter++)
51 : id2string(parameter.get_base_name());
53 id2string(function_name) + "::" + param_base_name;
54 parameter.set_base_name(param_base_name);
55 parameter.set_identifier(new_param_identifier);
58 new_param_sym.type = parameter.type();
61 new_param_sym.module = function_symbol.module;
62 new_param_sym.location = function_symbol.location;
63 symbol_table.add(new_param_sym);
64 }
65 }
67}
68
70{
71protected:
73 goto_functiont &function,
74 symbol_tablet &symbol_table,
75 const irep_idt &function_name) const override
76 {
77 auto const &function_symbol = symbol_table.lookup_ref(function_name);
78 source_locationt location = function_symbol.location;
79 location.set_function(function_name);
80
82 function.body.add(goto_programt::make_end_function(location));
83 }
84};
85
87{
88protected:
90 goto_functiont &function,
91 symbol_tablet &symbol_table,
92 const irep_idt &function_name) const override
93 {
94 auto const &function_symbol = symbol_table.lookup_ref(function_name);
95
97 annotated_location.set_function(function_name);
98 annotated_location.set_comment("undefined function should be unreachable");
99 annotated_location.set_property_class(ID_assertion);
100 function.body.add(
102
103 source_locationt location = function_symbol.location;
104 location.set_function(function_name);
105 function.body.add(goto_programt::make_end_function(location));
106 }
107};
108
111{
112protected:
114 goto_functiont &function,
115 symbol_tablet &symbol_table,
116 const irep_idt &function_name) const override
117 {
118 auto const &function_symbol = symbol_table.lookup_ref(function_name);
119
121 annotated_location.set_function(function_name);
122 annotated_location.set_comment("undefined function should be unreachable");
123 annotated_location.set_property_class(ID_assertion);
124 function.body.add(
126
127 source_locationt location = function_symbol.location;
128 location.set_function(function_name);
129 function.body.add(goto_programt::make_assumption(false_exprt(), location));
130 function.body.add(goto_programt::make_end_function(location));
131 }
132};
133
135{
136public:
149
162
163private:
165 const exprt &lhs,
166 const std::size_t initial_depth,
167 const source_locationt &source_location,
168 const irep_idt &function_id,
169 symbol_tablet &symbol_table,
170 goto_programt &dest) const
171 {
173 symbol_table,
174 source_location,
175 function_id,
178
179 code_blockt assignments;
180
181 symbol_factory.gen_nondet_init(
182 assignments,
183 lhs,
186 false); // do not initialize const objects at the top level
187
189
190 symbol_factory.declare_created_symbols(init_code);
191 init_code.append(assignments);
192
196
198 }
199
201 const std::string &param_name,
202 std::size_t param_number) const
203 {
204 if(parameters_to_havoc.has_value())
205 {
206 return std::regex_match(param_name, *parameters_to_havoc);
207 }
208 else
209 {
211 return std::binary_search(
212 param_numbers_to_havoc->begin(),
215 }
216 }
217
218protected:
220 goto_functiont &function,
221 symbol_tablet &symbol_table,
222 const irep_idt &function_name) const override
223 {
224 const namespacet ns(symbol_table);
225 // some user input checking
226 if(param_numbers_to_havoc.has_value() && !param_numbers_to_havoc->empty())
227 {
228 auto max_param_number = std::max_element(
230 if(*max_param_number >= function.parameter_identifiers.size())
231 {
233 "function " + id2string(function_name) + " does not take " +
234 std::to_string(*max_param_number + 1) + " arguments",
235 "--generate-havocing-body"};
236 }
237 for(const auto number : *param_numbers_to_havoc)
238 {
239 const auto &parameter = function.parameter_identifiers[number];
241 if(parameter_symbol.type.id() != ID_pointer)
242 {
244 "argument number " + std::to_string(number) + " of function " +
245 id2string(function_name) + " is not a pointer",
246 "--generate-havocing-body"};
247 }
248 }
249 }
250
251 auto const &function_symbol = symbol_table.lookup_ref(function_name);
252 source_locationt location = function_symbol.location;
253 location.set_function(function_name);
254
255 for(std::size_t i = 0; i < function.parameter_identifiers.size(); ++i)
256 {
257 const auto &parameter = function.parameter_identifiers[i];
259 if(
260 parameter_symbol.type.id() == ID_pointer &&
262 .base_type()
263 .get_bool(ID_C_constant) &&
265 {
266 auto goto_instruction =
269 parameter_symbol.symbol_expr(),
271 location));
272
273 dereference_exprt dereference_expr(
274 parameter_symbol.symbol_expr(),
275 to_pointer_type(parameter_symbol.type).base_type());
276
277 goto_programt dest;
279 dereference_expr,
280 1, // depth 1 since we pass the dereferenced pointer
281 location,
282 function_name,
283 symbol_table,
284 dest);
285
286 function.body.destructive_append(dest);
287
288 auto label_instruction =
289 function.body.add(goto_programt::make_skip(location));
290 goto_instruction->complete_goto(label_instruction);
291 }
292 }
293
294 for(auto const &global_id : globals_to_havoc)
295 {
296 auto const &global_sym = symbol_table.lookup_ref(global_id);
297
298 goto_programt dest;
299
302 0,
303 location,
304 irep_idt(),
305 symbol_table,
306 dest);
307
308 function.body.destructive_append(dest);
309 }
310
311 const typet &return_type = to_code_type(function_symbol.type).return_type();
312 if(return_type != empty_typet())
313 {
314 typet type(return_type);
315 type.remove(ID_C_constant);
316
318 type,
319 id2string(function_name),
320 "return_value",
321 location,
322 ID_C,
323 symbol_table);
324
325 aux_symbol.is_static_lifetime = false;
326
327 function.body.add(
328 goto_programt::make_decl(aux_symbol.symbol_expr(), location));
329
330 goto_programt dest;
331
333 aux_symbol.symbol_expr(),
334 0,
335 location,
336 function_name,
337 symbol_table,
338 dest);
339
340 function.body.destructive_append(dest);
341
343 typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type);
344
345 function.body.add(
347
348 function.body.add(
349 goto_programt::make_dead(aux_symbol.symbol_expr(), location));
350 }
351
352 function.body.add(goto_programt::make_end_function(location));
353
354 remove_skip(function.body);
355 }
356
357private:
358 const std::vector<irep_idt> globals_to_havoc;
363};
364
365class generate_function_bodies_errort : public std::runtime_error
366{
367public:
368 explicit generate_function_bodies_errort(const std::string &reason)
369 : runtime_error(reason)
370 {
371 }
372};
373
376std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory(
377 const std::string &options,
378 const c_object_factory_parameterst &object_factory_parameters,
379 const symbol_tablet &symbol_table,
380 message_handlert &message_handler)
381{
382 if(options.empty() || options == "nondet-return")
383 {
385 std::vector<irep_idt>{},
386 std::regex{},
387 object_factory_parameters,
388 message_handler);
389 }
390
391 if(options == "assume-false")
392 {
394 }
395
396 if(options == "assert-false")
397 {
399 }
400
401 if(options == "assert-false-assume-false")
402 {
403 return util_make_unique<
405 }
406
407 const std::vector<std::string> option_components = split_string(options, ',');
408 if(!option_components.empty() && option_components[0] == "havoc")
409 {
410 std::regex globals_regex;
411 std::regex params_regex;
412 std::vector<std::size_t> param_numbers;
413 for(std::size_t i = 1; i < option_components.size(); ++i)
414 {
415 const std::vector<std::string> key_value_pair =
417 if(key_value_pair.size() != 2)
418 {
420 "Expected key_value_pair of form argument:value");
421 }
422 if(key_value_pair[0] == "globals")
423 {
425 }
426 else if(key_value_pair[0] == "params")
427 {
429 if(param_identifiers.size() == 1)
430 {
433 if(!maybe_nondet_param_number.has_value())
434 {
436 continue;
437 }
438 }
439 std::transform(
440 param_identifiers.begin(),
441 param_identifiers.end(),
442 std::back_inserter(param_numbers),
443 [](const std::string &param_id) {
444 auto maybe_nondet_param_number = string2optional_size_t(param_id);
445 INVARIANT(
446 maybe_nondet_param_number.has_value(),
447 param_id + " not a number");
448 return *maybe_nondet_param_number;
449 });
450 std::sort(param_numbers.begin(), param_numbers.end());
451 }
452 else
453 {
455 "Unknown option \"" + key_value_pair[0] + "\"");
456 }
457 }
458 std::vector<irep_idt> globals_to_havoc;
459 namespacet ns(symbol_table);
460 messaget messages(message_handler);
461 const std::regex cprover_prefix = std::regex("__CPROVER.*");
462 for(auto const &symbol : symbol_table.symbols)
463 {
464 if(
465 symbol.second.is_lvalue && symbol.second.is_static_lifetime &&
466 std::regex_match(id2string(symbol.first), globals_regex))
467 {
468 if(std::regex_match(id2string(symbol.first), cprover_prefix))
469 {
470 messages.warning() << "generate function bodies: "
471 << "matched global '" << id2string(symbol.first)
472 << "' begins with __CPROVER, "
473 << "havoc-ing this global may interfere"
474 << " with analysis" << messaget::eom;
475 }
476 globals_to_havoc.push_back(symbol.first);
477 }
478 }
479 if(param_numbers.empty())
481 std::move(globals_to_havoc),
482 std::move(params_regex),
483 object_factory_parameters,
484 message_handler);
485 else
487 std::move(globals_to_havoc),
488 std::move(param_numbers),
489 object_factory_parameters,
490 message_handler);
491 }
492 throw generate_function_bodies_errort("Can't parse \"" + options + "\"");
493}
494
503 const std::regex &functions_regex,
504 const generate_function_bodiest &generate_function_body,
505 goto_modelt &model,
506 message_handlert &message_handler)
507{
508 messaget messages(message_handler);
509 const std::regex cprover_prefix = std::regex("__CPROVER.*");
510 bool did_generate_body = false;
511 for(auto &function : model.goto_functions.function_map)
512 {
513 if(
514 !function.second.body_available() &&
515 std::regex_match(id2string(function.first), functions_regex))
516 {
517 if(std::regex_match(id2string(function.first), cprover_prefix))
518 {
519 messages.warning() << "generate function bodies: matched function '"
520 << id2string(function.first)
521 << "' begins with __CPROVER "
522 << "the generated body for this function "
523 << "may interfere with analysis" << messaget::eom;
524 }
525 did_generate_body = true;
526 generate_function_body.generate_function_body(
527 function.second, model.symbol_table, function.first);
528 }
529 }
531 {
532 messages.warning()
533 << "generate function bodies: No function name matched regex"
534 << messaget::eom;
535 }
536}
537
539 const std::string &function_name,
540 const std::string &call_site_id,
541 const generate_function_bodiest &generate_function_body,
542 goto_modelt &model,
543 message_handlert &message_handler)
544{
545 PRECONDITION(!has_prefix(function_name, CPROVER_PREFIX));
547 PRECONDITION(call_site_number.has_value());
548
549 messaget messages(message_handler);
550
551 bool found = false;
553 typet function_type;
554
555 // get the mode and type from symbol table
556 for(auto const &symbol_pair : model.symbol_table)
557 {
558 auto const symbol = symbol_pair.second;
559 if(symbol.type.id() == ID_code && symbol.name == function_name)
560 {
561 function_mode = symbol.mode;
562 function_type = symbol.type;
563 found = true;
564 break;
565 }
566 }
568
569 // add function of the right name to the symbol table
572 havoc_function_symbol.pretty_name = function_name + "." + call_site_id;
573
574 havoc_function_symbol.is_lvalue = true;
576 havoc_function_symbol.type = function_type;
577
579
580 auto const &generated_havoc =
582
583 // convert to get the function stub to goto-model
584 goto_convert(model.symbol_table, model.goto_functions, message_handler);
585
586 // now generate body as above
587 for(auto &function : model.goto_functions.function_map)
588 {
589 if(
590 !function.second.body_available() &&
591 havoc_function_symbol.name == id2string(function.first))
592 {
593 generate_function_body.generate_function_body(
594 function.second, model.symbol_table, function.first);
595 }
596 }
597
598 auto is_havoc_function_call = [&function_name](const exprt &expr) {
599 if(expr.id() != ID_symbol)
600 return false;
601 std::string called_function_name =
602 id2string(to_symbol_expr(expr).get_identifier());
603 if(called_function_name == function_name)
604 return true;
605
606 return (has_prefix(called_function_name, function_name + "."));
607 };
608
609 // finally, rename the (right) call site
610 std::size_t counter = 0;
611 for(auto &function : model.goto_functions.function_map)
612 {
613 for(auto &instruction : function.second.body.instructions)
614 {
615 if(instruction.is_function_call())
616 {
617 auto &called_function = instruction.call_function();
618 if(is_havoc_function_call(called_function))
619 {
620 if(++counter == *call_site_number)
621 {
622 called_function = generated_havoc.symbol_expr();
623 return;
624 }
625 }
626 }
627 }
628 }
629}
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
C Nondet Symbol Factory.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
A codet representing sequential composition of program statements.
Definition std_code.h:130
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
The empty type.
Definition std_types.h:51
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
The Boolean constant false.
Definition std_expr.h:3017
generate_function_bodies_errort(const std::string &reason)
Base class for replace_function_body implementations.
void generate_function_body(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Replace the function body with one based on the replace_function_body class being used.
void generate_parameter_names(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const
Generate parameter names for unnamed parameters.
virtual void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const =0
Produce a body for the passed function At this point the body of function is always empty,...
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
bool body_available() const
void set_parameter_identifiers(const code_typet &code_type)
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.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_set_return_value(exprt return_value, const source_locationt &l=source_locationt::nil())
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::vector< std::size_t > param_numbers_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
const std::vector< irep_idt > globals_to_havoc
havoc_generate_function_bodiest(std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)
bool should_havoc_param(const std::string &param_name, std::size_t param_number) const
optionalt< std::vector< std::size_t > > param_numbers_to_havoc
void generate_function_body_impl(goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override
Produce a body for the passed function At this point the body of function is always empty,...
const c_object_factory_parameterst & object_factory_parameters
void havoc_expr_rec(const exprt &lhs, const std::size_t initial_depth, const source_locationt &source_location, const irep_idt &function_id, symbol_tablet &symbol_table, goto_programt &dest) const
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
void remove(const irep_idt &name)
Definition irep.cpp:95
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
message_handlert & get_message_handler()
Definition message.h:184
mstreamt & warning() const
Definition message.h:404
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The null pointer constant.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition symbol.h:179
void set_function(const irep_idt &function)
Expression to hold a symbol (variable)
Definition std_expr.h:113
std::set< irep_idt > recursion_sett
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition symbol.h:28
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
std::unique_ptr< generate_function_bodiest > generate_function_bodies_factory(const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
Create the type that actually generates the functions.
void generate_function_bodies(const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-...
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Program Transformation.
Goto Programs with Functions.
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
STL namespace.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
optionalt< std::size_t > string2optional_size_t(const std::string &str, int base)
Convert string to size_t similar to the stoul or stoull functions, return nullopt when the conversion...
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)