Skip to content

Commit 9d5688f

Browse files
NlightNFotishannes-steffenhagen-diffblue
NlightNFotis
and
hannes-steffenhagen-diffblue
committed
Add dynamic array handling
Create and non-det initialise of pointers to arrays making sure that they actually point at arrays. Also allows binding function parameters to the size of the array parameter. Only works with function parameters at the moment, not with struct members or globals. Also adds tests. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>
1 parent 0f96839 commit 9d5688f

File tree

19 files changed

+467
-11
lines changed

19 files changed

+467
-11
lines changed

‎regression/goto-harness/associated-size-parameter/main.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
3+
void test(int *array, int size)
4+
{
5+
for(int i = 0; i < size; i++)
6+
array[i] = i;
7+
8+
for(int i = 0; i < size; i++)
9+
assert(array[i] == i);
10+
}

‎regression/goto-harness/associated-size-parameter/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--harness-type call-function --function test --associated-array-size array:size
4+
VERIFICATION SUCCESSFUL
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--

‎regression/goto-harness/chain.sh

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,5 +23,11 @@ if [ -e "${name}-mod.gb" ] ; then
2323
rm -f "${name}-mod.gb"
2424
fi
2525

26-
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
27-
$cbmc --function $entry_point "${name}-mod.gb" --unwind 20 --unwinding-assertions
26+
# `# some comment` is an inline comment - basically, cause bash to execute an empty command
27+
28+
$goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args}
29+
$cbmc --function $entry_point "${name}-mod.gb" \
30+
--pointer-check `# because we want to see out of bounds errors` \
31+
--unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
32+
--unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
33+
# cbmc args end

‎regression/goto-harness/pointer-to-array-function-parameters-max-size/test.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <assert.h>
2+
void test(int *arr, int sz)
3+
{
4+
assert(sz < 10);
5+
for(int i = 0; i < sz; ++i)
6+
{
7+
arr[i] = 0;
8+
}
9+
}

‎regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
test.c
3+
--harness-type call-function --function test --max-array-size 10 --associated-array-size arr:sz
4+
\[test.assertion.1\] line \d+ assertion sz < 10: FAILURE
5+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
6+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
7+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
8+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
9+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
10+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
11+
^EXIT=10$
12+
^SIGNAL=0$
13+
--
14+
unwinding assertion loop \d: FAILURE

‎regression/goto-harness/pointer-to-array-function-parameters-min-size/test.c

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
#include <assert.h>
2+
3+
void min_array_size_test(int *arr, int sz)
4+
{
5+
assert(sz > 2);
6+
for(int i = 0; i < sz; ++i)
7+
{
8+
arr[i] = i;
9+
}
10+
for(int i = 0; i < sz; ++i)
11+
{
12+
assert(arr[i] == i);
13+
}
14+
}

‎regression/goto-harness/pointer-to-array-function-parameters-min-size/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--harness-type call-function --function min_array_size_test --max-array-size 3 --min-array-size 3 --associated-array-size arr:sz
4+
VERIFICATION SUCCESSFUL
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
unwinding assertion loop \d: FAILURE

‎regression/goto-harness/pointer-to-array-function-parameters-multi-arg-right/test.c

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#include <assert.h>
2+
3+
int is_prefix_of(
4+
const char *string,
5+
int string_size,
6+
const char *prefix,
7+
int prefix_size)
8+
{
9+
if(string_size < prefix_size)
10+
{
11+
return 0;
12+
}
13+
14+
for(int ix = 0; ix < prefix_size; ++ix)
15+
{
16+
if(string[ix] != prefix[ix])
17+
{
18+
return 0;
19+
}
20+
}
21+
return 1;
22+
}

‎regression/goto-harness/pointer-to-array-function-parameters-multi-arg-right/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
4+
^SIGNAL=0$
5+
^EXIT=0$
6+
VERIFICATION SUCCESSFUL
7+
--
8+
unwinding assertion loop \d+: FAILURE

‎regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.c

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <assert.h>
2+
#include <stddef.h>
3+
4+
int is_prefix_of(
5+
const char *string,
6+
size_t string_size,
7+
const char *prefix,
8+
size_t prefix_size)
9+
{
10+
if(string_size < prefix_size)
11+
{
12+
return 0;
13+
}
14+
assert(prefix_size <= string_size);
15+
// oh no! we should have used prefix_size here
16+
for(int ix = 0; ix < string_size; ++ix)
17+
{
18+
if(string[ix] != prefix[ix])
19+
{
20+
return 0;
21+
}
22+
}
23+
return 1;
24+
}

‎regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE
7+
VERIFICATION FAILED
8+
--

‎regression/goto-harness/pointer-to-array-function-parameters-with-size/test.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
void test(int *arr, int sz)
2+
{
3+
for(int i = 0; i < sz; ++i)
4+
{
5+
arr[i] = 0;
6+
}
7+
}

‎regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
test.c
3+
--harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
7+
\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
8+
\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
9+
\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
10+
\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
11+
\[test.pointer_dereference.6\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS
12+
--

‎regression/goto-harness/pointer-to-array-function-parameters/test.c

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#include <assert.h>
2+
3+
void test(int *arr)
4+
{
5+
// works because the arrays we generate have at least one element
6+
arr[0] = 5;
7+
8+
// doesn't work because our arrays have at most ten elements
9+
arr[10] = 10;
10+
}

‎regression/goto-harness/pointer-to-array-function-parameters/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
test.c
3+
--harness-type call-function --function test --treat-pointer-as-array arr
4+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS
5+
\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)10\]: FAILURE
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--

‎src/goto-harness/function_call_harness_generator.cpp

Lines changed: 108 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,10 @@ Author: Diffblue Ltd.
2121
#include <goto-programs/goto_convert.h>
2222
#include <goto-programs/goto_model.h>
2323

24+
#include <algorithm>
25+
#include <iterator>
26+
#include <set>
27+
2428
#include "function_harness_generator_options.h"
2529
#include "goto_harness_parse_options.h"
2630
#include "recursive_initialization.h"
@@ -41,6 +45,12 @@ struct function_call_harness_generatort::implt
4145
recursive_initialization_configt recursive_initialization_config;
4246
std::unique_ptr<recursive_initializationt> recursive_initialization;
4347

48+
std::set<irep_idt> function_parameters_to_treat_as_arrays;
49+
std::set<irep_idt> function_arguments_to_treat_as_arrays;
50+
51+
std::map<irep_idt, irep_idt> function_argument_to_associated_array_size;
52+
std::map<irep_idt, irep_idt> function_parameter_to_associated_array_size;
53+
4454
/// \see goto_harness_generatort::generate
4555
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name);
4656
/// Iterate over the symbol table and generate initialisation code for
@@ -117,6 +127,57 @@ void function_call_harness_generatort::handle_option(
117127
"--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT};
118128
}
119129
}
130+
else if(option == FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT)
131+
{
132+
p_impl->recursive_initialization_config.max_dynamic_array_size =
133+
require_one_size_value(
134+
FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT, values);
135+
}
136+
else if(option == FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT)
137+
{
138+
p_impl->recursive_initialization_config.min_dynamic_array_size =
139+
require_one_size_value(
140+
FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values);
141+
}
142+
else if(option == FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT)
143+
{
144+
p_impl->function_parameters_to_treat_as_arrays.insert(
145+
values.begin(), values.end());
146+
}
147+
else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT)
148+
{
149+
for(auto const &array_size_pair : values)
150+
{
151+
try
152+
{
153+
std::string array;
154+
std::string size;
155+
split_string(array_size_pair, ':', array, size);
156+
// --associated-array-size implies --treat-pointer-as-array
157+
// but it is not an error to specify both, so we don't check
158+
// for duplicates here
159+
p_impl->function_parameters_to_treat_as_arrays.insert(array);
160+
auto const inserted =
161+
p_impl->function_parameter_to_associated_array_size.emplace(
162+
array, size);
163+
if(!inserted.second)
164+
{
165+
throw invalid_command_line_argument_exceptiont{
166+
"can not have two associated array sizes for one array",
167+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
168+
}
169+
}
170+
catch(const deserialization_exceptiont &)
171+
{
172+
throw invalid_command_line_argument_exceptiont{
173+
"`" + array_size_pair +
174+
"' is in an invalid format for array size pair",
175+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT,
176+
"array_name:size_name, where both are the names of function "
177+
"parameters"};
178+
}
179+
}
180+
}
120181
else
121182
{
122183
throw invalid_command_line_argument_exceptiont{
@@ -145,7 +206,17 @@ void function_call_harness_generatort::implt::generate(
145206
code_blockt function_body{};
146207
auto const arguments = declare_arguments(function_body);
147208

209+
// configure and create recursive initialisation object
148210
recursive_initialization_config.mode = function_to_call.mode;
211+
recursive_initialization_config.pointers_to_treat_as_arrays =
212+
function_arguments_to_treat_as_arrays;
213+
recursive_initialization_config.array_name_to_associated_array_size_variable =
214+
function_argument_to_associated_array_size;
215+
for(const auto &pair : function_argument_to_associated_array_size)
216+
{
217+
recursive_initialization_config.variables_that_hold_array_sizes.insert(
218+
pair.second);
219+
}
149220
recursive_initialization = util_make_unique<recursive_initializationt>(
150221
recursive_initialization_config, goto_model);
151222

@@ -197,6 +268,15 @@ void function_call_harness_generatort::validate_options()
197268
throw invalid_command_line_argument_exceptiont{
198269
"required parameter entry function not set",
199270
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
271+
if(
272+
p_impl->recursive_initialization_config.min_dynamic_array_size >
273+
p_impl->recursive_initialization_config.max_dynamic_array_size)
274+
{
275+
throw invalid_command_line_argument_exceptiont{
276+
"min dynamic array size cannot be greater than max dynamic array size",
277+
"--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
278+
" --" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
279+
}
200280
}
201281

202282
std::size_t function_call_harness_generatort::require_one_size_value(
@@ -287,13 +367,41 @@ function_call_harness_generatort::implt::declare_arguments(
287367
function_to_call.location,
288368
"__goto_harness",
289369
*symbol_table};
370+
std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
290371
for(const auto &parameter : parameters)
291372
{
292373
auto argument = allocate_objects.allocate_automatic_local_object(
293374
parameter.type(), parameter.get_base_name());
375+
parameter_name_to_argument_name.insert(
376+
{parameter.get_base_name(), argument.get_identifier()});
294377
arguments.push_back(argument);
295378
}
296379

380+
for(const auto &pair : parameter_name_to_argument_name)
381+
{
382+
auto const &parameter_name = pair.first;
383+
auto const &argument_name = pair.second;
384+
if(function_parameters_to_treat_as_arrays.count(parameter_name) != 0)
385+
{
386+
function_arguments_to_treat_as_arrays.insert(argument_name);
387+
}
388+
auto it = function_parameter_to_associated_array_size.find(parameter_name);
389+
if(it != function_parameter_to_associated_array_size.end())
390+
{
391+
auto const &associated_array_size_parameter = it->second;
392+
auto associated_array_size_argument =
393+
parameter_name_to_argument_name.find(associated_array_size_parameter);
394+
if(
395+
associated_array_size_argument == parameter_name_to_argument_name.end())
396+
{
397+
throw invalid_command_line_argument_exceptiont{
398+
"associated array size is not there",
399+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
400+
}
401+
function_argument_to_associated_array_size.insert(
402+
{argument_name, associated_array_size_argument->second});
403+
}
404+
}
297405
allocate_objects.declare_created_symbols(function_body);
298406
return arguments;
299407
}

‎src/goto-harness/function_harness_generator_options.h

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,23 @@ Author: Diffblue Ltd.
1414
#define FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "min-null-tree-depth"
1515
#define FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \
1616
"max-nondet-tree-depth"
17+
#define FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size"
18+
#define FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size"
19+
#define FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \
20+
"treat-pointer-as-array"
21+
#define FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \
22+
"associated-array-size"
1723

1824
// clang-format off
1925
#define FUNCTION_HARNESS_GENERATOR_OPTIONS \
2026
"(" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT "):" \
2127
"(" FUNCTION_HARNESS_GENERATOR_NONDET_GLOBALS_OPT ")" \
2228
"(" FUNCTION_HARNESS_GENERATOR_MIN_NULL_TREE_DEPTH_OPT "):" \
2329
"(" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \
30+
"(" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \
31+
"(" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \
32+
"(" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT "):" \
33+
"(" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT "):" \
2434
// FUNCTION_HARNESS_GENERATOR_OPTIONS
2535

2636
// clang-format on
@@ -38,6 +48,20 @@ Author: Diffblue Ltd.
3848
"--" FUNCTION_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT \
3949
" N limit size of nondet (e.g. input) object tree;\n" \
4050
" at level N pointers are set to null\n" \
51+
"--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT \
52+
" N minimum size of dynamically created arrays (default: 1)\n" \
53+
"--" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \
54+
" N maximum size of dynamically created arrays (default: 2)\n" \
55+
"--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTER_AS_ARRAY_OPT \
56+
" parameter treat the function parameter with the name `parameter'\n" \
57+
" as an array\n" \
58+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \
59+
" array_name:size_name\n" \
60+
" set the parameter <size_name> to the size\n"\
61+
" of the array <array_name>\n" \
62+
" (implies " \
63+
"-- " FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT \
64+
" <array_name>)\n" \
4165
// FUNCTION_HARNESS_GENERATOR_HELP
4266

4367
// clang-format on

0 commit comments

Comments
 (0)