Skip to content

Commit e43ce92

Browse files
NlightNFotishannes-steffenhagen-diffblue
NlightNFotis
and
hannes-steffenhagen-diffblue
committed
Add support for nondet initialisation of strings.
Add support for nondet-initialisation of strings in the function-call goto-harness leveraging pointer nondet initialisation. Co-authored-by: Fotis Koutoulakis <fotis.koutoulakis@diffblue.com> Co-authored-by: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>
1 parent 272ba02 commit e43ce92

File tree

10 files changed

+203
-18
lines changed

10 files changed

+203
-18
lines changed

‎regression/goto-harness/nondet_strings/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
#include <assert.h>
2+
3+
void function(char *pointer, int size)
4+
{
5+
assert(pointer[size - 1] == '\0');
6+
}

‎regression/goto-harness/nondet_strings/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--harness-type call-function --function function --treat-pointer-as-cstring pointer --associated-array-size pointer:size
4+
\[function.assertion.\d+\] line \d+ assertion pointer\[size - 1\] == \'\\0\': SUCCESS
5+
^VERIFICATION SUCCESSFUL$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--

‎regression/goto-harness/nondet_strings_failing_assertion/main.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
3+
int stringlength(char *s)
4+
{
5+
int counter = 0;
6+
while(*s++ != 0)
7+
counter++;
8+
return counter;
9+
}
10+
11+
void calling_func(char *s, int length)
12+
{
13+
// WRONG: This should be stringlength(s)
14+
// +1 because length is going to be length
15+
// of the array, not the string
16+
assert(stringlength(s) == length);
17+
}

‎regression/goto-harness/nondet_strings_failing_assertion/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--harness-type call-function --function calling_func --treat-pointer-as-cstring s --associated-array-size s:length
4+
\[calling_func.assertion.\d+\] line \d+ assertion stringlength\(s\) == length: FAILURE
5+
^VERIFICATION FAILED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--

‎regression/goto-harness/nondet_strings_should_only_have_zero_at_end/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
int stringlength(char *s)
4+
{
5+
int counter = 0;
6+
while(*s++ != 0)
7+
counter++;
8+
return counter;
9+
}
10+
11+
void calling_func(char *s, int length)
12+
{
13+
// +1 because length is going to be length
14+
// of the array, not the string
15+
assert(stringlength(s) + 1 == length);
16+
}

‎regression/goto-harness/nondet_strings_should_only_have_zero_at_end/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--harness-type call-function --function calling_func --treat-pointer-as-cstring s --associated-array-size s:length
4+
\[calling_func.assertion.\d+\] line \d+ assertion stringlength\(s\) \+ 1 == length: SUCCESS
5+
^VERIFICATION SUCCESSFUL$
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--

‎src/goto-harness/function_call_harness_generator.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,9 @@ struct function_call_harness_generatort::implt
4848
std::set<irep_idt> function_parameters_to_treat_as_arrays;
4949
std::set<irep_idt> function_arguments_to_treat_as_arrays;
5050

51+
std::set<irep_idt> function_parameters_to_treat_as_cstrings;
52+
std::set<irep_idt> function_arguments_to_treat_as_cstrings;
53+
5154
std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
5255
std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
5356

@@ -178,6 +181,11 @@ void function_call_harness_generatort::handle_option(
178181
}
179182
}
180183
}
184+
else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING)
185+
{
186+
p_impl->function_parameters_to_treat_as_cstrings.insert(
187+
values.begin(), values.end());
188+
}
181189
else
182190
{
183191
throw invalid_command_line_argument_exceptiont{
@@ -217,6 +225,8 @@ void function_call_harness_generatort::implt::generate(
217225
recursive_initialization_config.variables_that_hold_array_sizes.insert(
218226
pair.second);
219227
}
228+
recursive_initialization_config.pointers_to_treat_as_cstrings =
229+
function_arguments_to_treat_as_cstrings;
220230
recursive_initialization = util_make_unique<recursive_initializationt>(
221231
recursive_initialization_config, goto_model);
222232

@@ -385,6 +395,12 @@ function_call_harness_generatort::implt::declare_arguments(
385395
{
386396
function_arguments_to_treat_as_arrays.insert(argument_name);
387397
}
398+
399+
if(function_parameters_to_treat_as_cstrings.count(parameter_name) != 0)
400+
{
401+
function_arguments_to_treat_as_cstrings.insert(argument_name);
402+
}
403+
388404
auto it = function_parameter_to_associated_array_size.find(parameter_name);
389405
if(it != function_parameter_to_associated_array_size.end())
390406
{

‎src/goto-harness/function_harness_generator_options.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,8 @@ Author: Diffblue Ltd.
2020
"treat-pointer-as-array"
2121
#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \
2222
"associated-array-size"
23+
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING \
24+
"treat-pointer-as-cstring"
2325

2426
// clang-format off
2527
#define FUNCTION_HARNESS_GENERATOR_OPTIONS \
@@ -31,6 +33,7 @@ Author: Diffblue Ltd.
3133
"(" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \
3234
"(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):" \
3335
"(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):" \
36+
"(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_CSTRING "):" \
3437
// FUNCTION_HARNESS_GENERATOR_OPTIONS
3538

3639
// clang-format on

‎src/goto-harness/recursive_initialization.cpp

Lines changed: 98 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,8 @@ Author: Diffblue Ltd.
1717
#include <util/std_code.h>
1818
#include <util/std_expr.h>
1919

20+
#include <functional>
21+
2022
recursive_initializationt::recursive_initializationt(
2123
recursive_initialization_configt initialization_config,
2224
goto_modelt &goto_model)
@@ -38,20 +40,27 @@ void recursive_initializationt::initialize(
3840
}
3941
else if(type.id() == ID_pointer)
4042
{
41-
if(
42-
lhs.id() == ID_symbol &&
43-
should_be_treated_as_array(to_symbol_expr(lhs).get_identifier()))
43+
if(lhs.id() == ID_symbol)
4444
{
45-
initialize_dynamic_array(lhs, depth, known_tags, body);
46-
}
47-
else
48-
{
49-
initialize_pointer(lhs, depth, known_tags, body);
45+
auto const &lhs_symbol = to_symbol_expr(lhs);
46+
if(should_be_treated_as_cstring(lhs_symbol.get_identifier()))
47+
{
48+
initialize_cstring(lhs, depth, known_tags, body);
49+
return;
50+
}
51+
else if(should_be_treated_as_array(lhs_symbol.get_identifier()))
52+
{
53+
initialize_dynamic_array(
54+
lhs, depth, known_tags, body, default_array_member_initialization());
55+
return;
56+
}
5057
}
58+
initialize_pointer(lhs, depth, known_tags, body);
5159
}
5260
else if(type.id() == ID_array)
5361
{
54-
initialize_array(lhs, depth, known_tags, body);
62+
initialize_array(
63+
lhs, depth, known_tags, body, default_array_member_initialization());
5564
}
5665
else
5766
{
@@ -163,19 +172,17 @@ void recursive_initializationt::initialize_array(
163172
const exprt &array,
164173
const std::size_t depth,
165174
const recursion_sett &known_tags,
166-
code_blockt &body)
175+
code_blockt &body,
176+
array_convertert array_member_initialization)
167177
{
168178
PRECONDITION(array.type().id() == ID_array);
169179
const auto &array_type = to_array_type(array.type());
170180
const auto array_size =
171181
numeric_cast_v<std::size_t>(to_constant_expr(array_type.size()));
172182
for(std::size_t index = 0; index < array_size; index++)
173183
{
174-
initialize(
175-
index_exprt(array, from_integer(index, size_type())),
176-
depth,
177-
known_tags,
178-
body);
184+
array_member_initialization(
185+
array, array_size, index, depth, known_tags, body);
179186
}
180187
}
181188

@@ -202,11 +209,19 @@ optionalt<irep_idt> recursive_initializationt::get_associated_size_variable(
202209
array_name);
203210
}
204211

212+
bool recursive_initializationt::should_be_treated_as_cstring(
213+
const irep_idt &pointer_name) const
214+
{
215+
return initialization_config.pointers_to_treat_as_cstrings.count(
216+
pointer_name) != 0;
217+
}
218+
205219
void recursive_initializationt::initialize_dynamic_array(
206220
const exprt &pointer,
207221
const std::size_t depth,
208222
const recursion_sett &known_tags,
209-
code_blockt &body)
223+
code_blockt &body,
224+
array_convertert array_initialization)
210225
{
211226
PRECONDITION(pointer.type().id() == ID_pointer);
212227

@@ -269,7 +284,8 @@ void recursive_initializationt::initialize_dynamic_array(
269284
std::size_t array_counter = 0;
270285
for(const auto &array_variable : array_variables)
271286
{
272-
initialize(array_variable, depth + 1, known_tags, body);
287+
initialize_array(
288+
array_variable, depth + 1, known_tags, body, array_initialization);
273289
body.add(code_assignt{
274290
index_exprt{arrays, from_integer(array_counter++, size_type())},
275291
address_of_exprt{
@@ -303,6 +319,16 @@ void recursive_initializationt::initialize_dynamic_array(
303319
body.add(code_assignt{pointer, index_exprt{arrays, nondet_index}});
304320
}
305321

322+
void recursive_initializationt::initialize_cstring(
323+
const exprt &pointer,
324+
std::size_t depth,
325+
const recursion_sett &known_tags,
326+
code_blockt &body)
327+
{
328+
initialize_dynamic_array(
329+
pointer, depth, known_tags, body, cstring_member_initialization());
330+
}
331+
306332
std::string recursive_initialization_configt::to_string() const
307333
{
308334
std::ostringstream out{};
@@ -332,6 +358,61 @@ std::string recursive_initialization_configt::to_string() const
332358
<< associated_array_size.second;
333359
}
334360
out << "\n ]";
361+
out << "\n pointers_to_treat_as_cstrings = [";
362+
for(const auto &pointer_to_treat_as_string_name :
363+
pointers_to_treat_as_cstrings)
364+
{
365+
out << "\n " << pointer_to_treat_as_string_name << std::endl;
366+
}
367+
out << "\n ]";
335368
out << "\n}";
336369
return out.str();
337370
}
371+
372+
recursive_initializationt::array_convertert
373+
recursive_initializationt::default_array_member_initialization()
374+
{
375+
return [this](
376+
const exprt &array,
377+
const std::size_t length,
378+
const std::size_t current_index,
379+
const std::size_t depth,
380+
const recursion_sett &known_tags,
381+
code_blockt &body) {
382+
PRECONDITION(array.type().id() == ID_array);
383+
initialize(
384+
index_exprt{array, from_integer(current_index, size_type())},
385+
depth,
386+
known_tags,
387+
body);
388+
};
389+
}
390+
391+
recursive_initializationt::array_convertert
392+
recursive_initializationt::cstring_member_initialization()
393+
{
394+
return [this](
395+
const exprt &array,
396+
const std::size_t length,
397+
const std::size_t current_index,
398+
const std::size_t depth,
399+
const recursion_sett &known_tags,
400+
code_blockt &body) {
401+
PRECONDITION(array.type().id() == ID_array);
402+
PRECONDITION(array.type().subtype() == char_type());
403+
auto const member =
404+
index_exprt{array, from_integer(current_index, size_type())};
405+
if(current_index + 1 == length)
406+
{
407+
body.add(code_assignt{member, from_integer(0, array.type().subtype())});
408+
}
409+
else
410+
{
411+
initialize(member, depth, known_tags, body);
412+
// We shouldn't have `\0` anywhere but at the end of a string.
413+
body.add(
414+
code_assumet{
415+
notequal_exprt{member, from_integer(0, array.type().subtype())}});
416+
}
417+
};
418+
}

‎src/goto-harness/recursive_initialization.h

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,8 @@ struct recursive_initialization_configt
3232
std::set<irep_idt> variables_that_hold_array_sizes;
3333
std::map<irep_idt, irep_idt> array_name_to_associated_array_size_variable;
3434

35+
std::set<irep_idt> pointers_to_treat_as_cstrings;
36+
3537
std::string to_string() const; // for debugging purposes
3638
};
3739

@@ -81,12 +83,31 @@ class recursive_initializationt
8183
std::size_t depth,
8284
const recursion_sett &known_tags,
8385
code_blockt &body);
86+
87+
using array_convertert = std::function<void(
88+
const exprt &pointer,
89+
std::size_t length,
90+
std::size_t current_index,
91+
std::size_t depth,
92+
const recursion_sett &known_tags,
93+
code_blockt &body)>;
94+
array_convertert default_array_member_initialization();
95+
array_convertert cstring_member_initialization();
96+
8497
void initialize_array(
8598
const exprt &array,
8699
std::size_t depth,
87100
const recursion_sett &known_tags,
88-
code_blockt &body);
101+
code_blockt &body,
102+
array_convertert array_member_initialization);
89103
void initialize_dynamic_array(
104+
const exprt &pointer,
105+
std::size_t depth,
106+
const recursion_sett &known_tags,
107+
code_blockt &body,
108+
array_convertert array_member_initialization);
109+
110+
void initialize_cstring(
90111
const exprt &pointer,
91112
std::size_t depth,
92113
const recursion_sett &known_tags,
@@ -96,6 +117,7 @@ class recursive_initializationt
96117
bool is_array_size_parameter(const irep_idt &cmdline_arg) const;
97118
optionalt<irep_idt>
98119
get_associated_size_variable(const irep_idt &array_name) const;
120+
bool should_be_treated_as_cstring(const irep_idt &pointer_name) const;
99121
};
100122

101123
#endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H

0 commit comments

Comments
 (0)