Skip to content

Commit 18be548

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 5829ee6 commit 18be548

File tree

19 files changed

+464
-6
lines changed

19 files changed

+464
-6
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: 116 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,61 @@ 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+
std::copy(
145+
values.begin(),
146+
values.end(),
147+
std::inserter(
148+
p_impl->function_parameters_to_treat_as_arrays,
149+
p_impl->function_parameters_to_treat_as_arrays.end()));
150+
}
151+
else if(option == FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT)
152+
{
153+
for(auto const &array_size_pair : values)
154+
{
155+
std::string array;
156+
std::string size;
157+
try
158+
{
159+
split_string(array_size_pair, ':', array, size);
160+
// --associated-array-size implies --treat-pointer-as-array
161+
// but it is not an error to specify both, so we don't check
162+
// for duplicates here
163+
p_impl->function_parameters_to_treat_as_arrays.insert(array);
164+
auto const inserted =
165+
p_impl->function_parameter_to_associated_array_size.insert(
166+
{array, size});
167+
if(!inserted.second)
168+
{
169+
throw invalid_command_line_argument_exceptiont{
170+
"can not have two associated array sizes for one array",
171+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
172+
}
173+
}
174+
catch(const deserialization_exceptiont &)
175+
{
176+
throw invalid_command_line_argument_exceptiont{
177+
"`" + array_size_pair +
178+
"' is in an invalid format for array size pair",
179+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT,
180+
"array_name:size_name, where both are the names of function "
181+
"parameters"};
182+
}
183+
}
184+
}
120185
else
121186
{
122187
throw invalid_command_line_argument_exceptiont{
@@ -145,7 +210,19 @@ void function_call_harness_generatort::implt::generate(
145210
code_blockt function_body{};
146211
auto const arguments = declare_arguments(function_body);
147212

213+
// configure and create recursive initialisation object
148214
recursive_initialization_config.mode = function_to_call.mode;
215+
recursive_initialization_config.pointers_to_treat_as_arrays =
216+
function_arguments_to_treat_as_arrays;
217+
recursive_initialization_config.array_name_to_associated_array_size_variable =
218+
function_argument_to_associated_array_size;
219+
std::transform(
220+
function_argument_to_associated_array_size.begin(),
221+
function_argument_to_associated_array_size.end(),
222+
std::inserter(
223+
recursive_initialization_config.variables_that_hold_array_sizes,
224+
recursive_initialization_config.variables_that_hold_array_sizes.end()),
225+
[](const std::pair<irep_idt, irep_idt> &p) { return p.second; });
149226
recursive_initialization = util_make_unique<recursive_initializationt>(
150227
recursive_initialization_config, goto_model);
151228

@@ -197,6 +274,15 @@ void function_call_harness_generatort::validate_options()
197274
throw invalid_command_line_argument_exceptiont{
198275
"required parameter entry function not set",
199276
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
277+
if(
278+
p_impl->recursive_initialization_config.min_dynamic_array_size >
279+
p_impl->recursive_initialization_config.max_dynamic_array_size)
280+
{
281+
throw invalid_command_line_argument_exceptiont{
282+
"min dynamic array size cannot be greater than max dynamic array size",
283+
"--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
284+
" --" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
285+
}
200286
}
201287

202288
std::size_t function_call_harness_generatort::require_one_size_value(
@@ -287,13 +373,43 @@ function_call_harness_generatort::implt::declare_arguments(
287373
function_to_call.location,
288374
"__goto_harness",
289375
*symbol_table};
376+
std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
290377
for(const auto &parameter : parameters)
291378
{
292379
auto argument = allocate_objects.allocate_automatic_local_object(
293380
parameter.type(), parameter.get_base_name());
381+
parameter_name_to_argument_name.insert(
382+
{parameter.get_base_name(), argument.get_identifier()});
294383
arguments.push_back(argument);
295384
}
296385

386+
for(const auto &p : parameter_name_to_argument_name)
387+
{
388+
auto const &parameter_name = p.first;
389+
auto const &argument_name = p.second;
390+
if(
391+
function_parameters_to_treat_as_arrays.find(parameter_name) !=
392+
function_parameters_to_treat_as_arrays.end())
393+
{
394+
function_arguments_to_treat_as_arrays.insert(argument_name);
395+
}
396+
auto it = function_parameter_to_associated_array_size.find(parameter_name);
397+
if(it != function_parameter_to_associated_array_size.end())
398+
{
399+
auto const &associated_array_size_parameter = it->second;
400+
auto associated_array_size_argument =
401+
parameter_name_to_argument_name.find(associated_array_size_parameter);
402+
if(
403+
associated_array_size_argument == parameter_name_to_argument_name.end())
404+
{
405+
throw invalid_command_line_argument_exceptiont{
406+
"associated array size is not there",
407+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
408+
}
409+
function_argument_to_associated_array_size.insert(
410+
{argument_name, associated_array_size_argument->second});
411+
}
412+
}
297413
allocate_objects.declare_created_symbols(function_body);
298414
return arguments;
299415
}

‎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)