Skip to content

Commit ca0553a

Browse files
hannes-steffenhagen-diffbluehannes-steffenhagen-diffblue
committed
WIP Address thomas comments
1 parent cc7f288 commit ca0553a

File tree

7 files changed

+132
-88
lines changed

7 files changed

+132
-88
lines changed

‎regression/goto-instrument/generate-function-body/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,4 @@ main.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
^\[main.assertion.1\] assertion does_not_get_reached: SUCCESS$
8-
^\[should_be_generated.assertion.1\] assertion FALSE: FAILURE$
8+
^\[should_be_generated.assertion.1\] assertion FALSE: FAILURE$

‎src/goto-instrument/goto_instrument_parse_options.cpp

+5-13
Original file line numberDiff line numberDiff line change
@@ -1464,7 +1464,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
14641464
std::regex function_regex = std::regex(
14651465
only_generate ? cmdline.get_value("generate-function-body")
14661466
: cmdline.get_value("replace-function-body"));
1467-
status() << "Replacing function bodies" << eom;
1467+
status() << (only_generate ? "Generating" : "Replacing")
1468+
<< " function bodies" << eom;
14681469
replace_function_bodies(
14691470
goto_model.goto_functions,
14701471
goto_model.symbol_table,
@@ -1551,18 +1552,9 @@ void goto_instrument_parse_optionst::help()
15511552
" --undefined-function-is-assume-false\n"
15521553
// NOLINTNEXTLINE(whitespace/line_length)
15531554
" convert each call to an undefined function to assume(false)\n"
1554-
" --replace-function-body <regex>\n"
1555-
// NOLINTNEXTLINE(whitespace/line_length)
1556-
" Replace bodies of function matching regex\n"
1557-
" --generate-function-body <regex>\n"
1558-
// NOLINTNEXTLINE(whitespace/line_length)
1559-
" Like replace-function-body, but ignore functions that already have bodies\n"
1560-
" --replace-function-body-options <option>\n"
1561-
// NOLINTNEXTLINE(whitespace/line_length)
1562-
" One of empty, assert-false, assume-false, nondet-return\n"
1563-
" assert-false-assume-false and\n"
1564-
// NOLINTNEXTLINE(whitespace/line_length)
1565-
" havoc[,params:<regex>][,globals:<regex>]"
1555+
HELP_REPLACE_FUNCTION_BODY
1556+
HELP_GENERATE_FUNCTION_BODY
1557+
HELP_REPLACE_FUNCTION_BODY_OPTIONS
15661558
"\n"
15671559
"Loop transformations:\n"
15681560
" --k-induction <k> check loops with k-induction\n"

‎src/goto-instrument/goto_instrument_parse_options.h

+5-3
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,8 @@ Author: Daniel Kroening, [email protected]
2424

2525
#include <analyses/goto_check.h>
2626

27+
#include <goto-instrument/replace_function_bodies.h>
28+
2729
// clang-format off
2830
#define GOTO_INSTRUMENT_OPTIONS \
2931
"(all)" \
@@ -87,9 +89,9 @@ Author: Daniel Kroening, [email protected]
8789
"(remove-function-body):"\
8890
"(splice-call):" \
8991
OPT_REMOVE_CALLS_NO_BODY \
90-
"(replace-function-body):" \
91-
"(generate-function-body):" \
92-
"(replace-function-body-options):"
92+
OPT_REPLACE_FUNCTION_BODY \
93+
OPT_GENERATE_FUNCTION_BODY \
94+
OPT_REPLACE_FUNCTION_BODY_OPTIONS
9395

9496
// clang-format on
9597

‎src/goto-instrument/replace_function_bodies.cpp

+54-71
Original file line numberDiff line numberDiff line change
@@ -16,10 +16,18 @@ Author: DiffBlue Limited.
1616
#include <util/make_unique.h>
1717
#include <util/message.h>
1818
#include <langapi/language_util.h>
19+
#include <util/string_utils.h>
1920

21+
/// Base class for replace_function_body implementations
2022
class replace_function_bodiest
2123
{
2224
protected:
25+
/// Produce a body for the passed function
26+
/// At this point the body of function is always empty,
27+
/// and all function parameters have identifiers
28+
/// @param function whose body to generate
29+
/// @param symbol_table of the current goto program
30+
/// @param function_name Identifier of function
2331
virtual void generate_function_body(
2432
goto_functiont &function,
2533
symbol_tablet &symbol_table,
@@ -28,6 +36,11 @@ class replace_function_bodiest
2836
public:
2937
virtual ~replace_function_bodiest() = default;
3038

39+
/// Replace the function body with one based on the implementation
40+
/// This will work the same whether or not the function already has a body
41+
/// @param function whose body to replace
42+
/// @param symbol_table of the current goto program
43+
/// @param function_name Identifier of function
3144
void replace_function_body(
3245
goto_functiont &function,
3346
symbol_tablet &symbol_table,
@@ -51,37 +64,29 @@ class replace_function_bodiest
5164
int param_counter = 0;
5265
for(auto &parameter : function.type.parameters())
5366
{
54-
if(
55-
parameter.type().id() == ID_pointer &&
56-
!is_constant_or_has_constant_components(parameter.type(), ns))
67+
if(parameter.get_identifier().empty())
5768
{
58-
if(parameter.get_identifier().empty())
59-
{
60-
const std::string param_base_name =
61-
parameter.get_base_name().empty()
62-
? "__param$" + std::to_string(param_counter++)
63-
: id2string(parameter.get_base_name());
64-
irep_idt new_param_identifier =
65-
id2string(function_name) + "::" + param_base_name;
66-
parameter.set_base_name(param_base_name);
67-
parameter.set_identifier(new_param_identifier);
68-
parameter_symbolt new_param_sym;
69-
new_param_sym.name = new_param_identifier;
70-
new_param_sym.type = parameter.type();
71-
new_param_sym.base_name = param_base_name;
72-
new_param_sym.is_parameter = true;
73-
new_param_sym.mode = ID_C;
74-
const symbolt *function_symbol = symbol_table.lookup(function_name);
75-
new_param_sym.module = function_symbol->module;
76-
new_param_sym.location = function_symbol->location;
77-
symbol_table.add(new_param_sym);
78-
}
79-
auto function_symbol = *symbol_table.lookup(function_name);
80-
function_symbol.type = function.type;
81-
symbol_table.remove(function_name);
82-
symbol_table.insert(function_symbol);
69+
const std::string param_base_name =
70+
parameter.get_base_name().empty()
71+
? "__param$" + std::to_string(param_counter++)
72+
: id2string(parameter.get_base_name());
73+
irep_idt new_param_identifier =
74+
id2string(function_name) + "::" + param_base_name;
75+
parameter.set_base_name(param_base_name);
76+
parameter.set_identifier(new_param_identifier);
77+
parameter_symbolt new_param_sym;
78+
new_param_sym.name = new_param_identifier;
79+
new_param_sym.type = parameter.type();
80+
new_param_sym.base_name = param_base_name;
81+
new_param_sym.mode = ID_C;
82+
auto &function_symbol = symbol_table.lookup_ref(function_name);
83+
new_param_sym.module = function_symbol.module;
84+
new_param_sym.location = function_symbol.location;
85+
symbol_table.add(new_param_sym);
8386
}
8487
}
88+
auto &function_symbol = symbol_table.get_writeable_ref(function_name);
89+
function_symbol.type = function.type;
8590
}
8691
};
8792

@@ -184,7 +189,8 @@ class havoc_replace_function_bodiest : public replace_function_bodiest
184189
{
185190
if(
186191
parameter.type().id() == ID_pointer &&
187-
!parameter.type().subtype().get_bool(ID_C_constant) &&
192+
!is_constant_or_has_constant_components(
193+
parameter.type().subtype(), ns) &&
188194
std::regex_match(
189195
id2string(parameter.get_base_name()), parameters_to_havoc))
190196
{
@@ -222,44 +228,20 @@ class havoc_replace_function_bodiest : public replace_function_bodiest
222228
std::regex parameters_to_havoc;
223229
};
224230

225-
static std::vector<std::string>
226-
tokenize(const std::string &base, char separator)
231+
class replace_function_bodies_errort : public std::runtime_error
227232
{
228-
std::vector<std::string> tokens;
229-
tokens.push_back("");
230-
for(char c : base)
233+
public:
234+
replace_function_bodies_errort(
235+
const std::string &file,
236+
int line,
237+
const std::string &reason)
238+
: runtime_error(file + ":" + std::to_string(line) + ": " + reason)
231239
{
232-
if(c == separator)
233-
{
234-
tokens.push_back("");
235-
}
236-
else
237-
{
238-
tokens.back().push_back(c);
239-
}
240240
}
241-
return tokens;
242-
}
243-
244-
static void write_to_stream(std::ostream &out)
245-
{
246-
}
247-
248-
template <typename T, typename... Ts>
249-
void write_to_stream(std::ostream &out, const T &arg, const Ts &... args)
250-
{
251-
out << arg;
252-
write_to_stream(out, args...);
253-
}
241+
};
254242

255-
template <typename... Ts>
256-
std::string replace_function_body_parse_error(const Ts &... args)
257-
{
258-
std::ostringstream out;
259-
write_to_stream(
260-
out, "parse error for --replace-function-body-options: ", args...);
261-
return out.str();
262-
}
243+
#define REPLACE_FUNCTION_BODIES_ERROR(reason) \
244+
replace_function_bodies_errort(__FILE__, __LINE__, (reason))
263245

264246
std::unique_ptr<replace_function_bodiest> replace_function_body_options_factory(
265247
const std::string &options,
@@ -292,17 +274,18 @@ std::unique_ptr<replace_function_bodiest> replace_function_body_options_factory(
292274
return util_make_unique<empty_replace_function_bodiest>();
293275
}
294276

295-
const std::vector<std::string> tokens = tokenize(options, ',');
296-
if(!tokens.empty() && tokens[0] == "havoc")
277+
const std::vector<std::string> option_components = split_string(options, ',');
278+
if(!option_components.empty() && option_components[0] == "havoc")
297279
{
298280
std::regex globals_regex;
299281
std::regex params_regex;
300-
for(std::size_t i = 1; i < tokens.size(); ++i)
282+
for(std::size_t i = 1; i < option_components.size(); ++i)
301283
{
302-
const std::vector<std::string> key_value_pair = tokenize(tokens[i], ':');
284+
const std::vector<std::string> key_value_pair =
285+
split_string(option_components[i], ':');
303286
if(key_value_pair.size() != 2)
304287
{
305-
throw replace_function_body_parse_error(
288+
throw REPLACE_FUNCTION_BODIES_ERROR(
306289
"Expected key_value_pair of form argument:value");
307290
}
308291
if(key_value_pair[0] == "globals")
@@ -315,8 +298,8 @@ std::unique_ptr<replace_function_bodiest> replace_function_body_options_factory(
315298
}
316299
else
317300
{
318-
throw replace_function_body_parse_error(
319-
"Unknown option \"", key_value_pair[0], "\"");
301+
throw REPLACE_FUNCTION_BODIES_ERROR(
302+
"Unknown option \"" + key_value_pair[0] + "\"");
320303
}
321304
}
322305
std::vector<irep_idt> globals_to_havoc;
@@ -333,7 +316,7 @@ std::unique_ptr<replace_function_bodiest> replace_function_body_options_factory(
333316
return util_make_unique<havoc_replace_function_bodiest>(
334317
globals_to_havoc, params_regex);
335318
}
336-
throw replace_function_body_parse_error("Can't parse \"", options, "\"");
319+
throw REPLACE_FUNCTION_BODIES_ERROR("Can't parse \"" + options + "\"");
337320
}
338321

339322
void replace_function_bodies(

‎src/goto-instrument/replace_function_bodies.h

+58
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,43 @@ Author: DiffBlue Limited.
1818
#include <util/std_types.h>
1919
#include <util/message.h>
2020

21+
/// Replace function bodies with some default behavior
22+
/// Can generate the following types of function bodies:
23+
///
24+
/// assert-false: { __CPROVER_assert(false); }
25+
///
26+
/// assume-false: { __CPROVER_assume(false); }
27+
///
28+
/// assert-false-assume-false: {
29+
/// __CPROVER_assert(false);
30+
/// __CPROVER_assume(false); }
31+
///
32+
/// havoc[,params:<regex>][,globals:<regex>]:
33+
/// Assign nondet to the targets of pointer-to-non-const parameters
34+
/// matching regex, and non-const globals matching regex and then
35+
/// return nondet for non-void functions, e.g.:
36+
///
37+
/// int global; const int c_global;
38+
/// int function(int *param, const int *const_param);
39+
///
40+
/// havoc,params:(?!__).*,globals:(?!__).* (where (?!__) means
41+
/// "not preceded by __", which is recommended to avoid overwrite
42+
/// internal symbols), leads to
43+
///
44+
/// int function(int *param, consnt int *const_param) {
45+
/// *param = nondet_int();
46+
/// global = nondet_int();
47+
/// return nondet_int();
48+
/// }
49+
///
50+
/// nondet-return return nondet for non-void functions
51+
///
52+
/// @param functions The function container whose functions should be replaced
53+
/// @param symbol_table The symbol table of the goto program
54+
/// @param functions_regex Replace bodies of functions whose names matches regex
55+
/// @param only_generate When true, skip functions that already have a body
56+
/// @param replace_options Options string indicating what body to generate
57+
/// @param messages Destination for status/warning messages
2158
void replace_function_bodies(
2259
goto_functionst &functions,
2360
symbol_tablet &symbol_table,
@@ -26,4 +63,25 @@ void replace_function_bodies(
2663
const std::string &replace_options,
2764
messaget &messages);
2865

66+
#define OPT_REPLACE_FUNCTION_BODY "(replace-function-body):"
67+
#define OPT_GENERATE_FUNCTION_BODY "(generate-function-body):"
68+
#define OPT_REPLACE_FUNCTION_BODY_OPTIONS "(replace-function-body-options):"
69+
70+
#define HELP_REPLACE_FUNCTION_BODY \
71+
" --replace-function-body <regex>\n" \
72+
" Replace bodies of function matching regex\n"
73+
74+
#define HELP_GENERATE_FUNCTION_BODY \
75+
" --generate-function-body <regex>\n" \
76+
" Like replace-function-body, but ignore " \
77+
"functions that already have bodies\n"
78+
79+
#define HELP_REPLACE_FUNCTION_BODY_OPTIONS \
80+
" --replace-function-body-options <option>\n" \
81+
" One of empty, assert-false, assume-false, " \
82+
"nondet-return\n" \
83+
" assert-false-assume-false and\n" \
84+
" havoc[,params:<regex>][,globals:<regex>]\n" \
85+
" (default: nondet-return)"
86+
2987
#endif // CPROVER_GOTO_INSTRUMENT_REPLACE_FUNCTION_BODIES_H

‎src/util/string_utils.cpp

+7
Original file line numberDiff line numberDiff line change
@@ -99,6 +99,13 @@ void split_string(
9999
right=result[1];
100100
}
101101

102+
std::vector<std::string> split_string(const std::string &s, char delim)
103+
{
104+
std::vector<std::string> result;
105+
split_string(s, delim, result);
106+
return result;
107+
}
108+
102109
std::string trim_from_last_delimiter(
103110
const std::string &s,
104111
const char delim)

‎src/util/string_utils.h

+2
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ void split_string(
3030
std::string &right,
3131
bool strip=false);
3232

33+
std::vector<std::string> split_string(const std::string &s, char delim);
34+
3335
std::string trim_from_last_delimiter(
3436
const std::string &s,
3537
const char delim);

0 commit comments

Comments
 (0)