Skip to content

Commit 0089678

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 1fe074f commit 0089678

File tree

19 files changed

+459
-6
lines changed

19 files changed

+459
-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"
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: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
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

‎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: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
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

‎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: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
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+
--

‎src/goto-harness/function_call_harness_generator.cpp

Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,12 @@ struct function_call_harness_generatort::implt
4242
recursive_initialization_configt recursive_initialization_config;
4343
std::unique_ptr<recursive_initializationt> recursive_initialization;
4444

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

146207
recursive_initialization_config.mode = function_to_call.mode;
208+
recursive_initialization_config.pointers_to_treat_as_arrays =
209+
function_arguments_to_treat_as_arrays;
210+
recursive_initialization_config.array_name_to_associated_array_size_variable =
211+
function_argument_to_associated_array_size;
212+
std::transform(
213+
function_argument_to_associated_array_size.begin(),
214+
function_argument_to_associated_array_size.end(),
215+
std::inserter(
216+
recursive_initialization_config.variables_that_hold_array_sizes,
217+
recursive_initialization_config.variables_that_hold_array_sizes.end()),
218+
[](const std::pair<irep_idt, irep_idt> &p) { return p.second; });
147219
recursive_initialization = util_make_unique<recursive_initializationt>(
148220
recursive_initialization_config, goto_model);
149221

@@ -183,6 +255,15 @@ void function_call_harness_generatort::validate_options()
183255
throw invalid_command_line_argument_exceptiont{
184256
"required parameter entry function not set",
185257
"--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT};
258+
if(
259+
p_impl->recursive_initialization_config.min_dynamic_array_size >
260+
p_impl->recursive_initialization_config.max_dynamic_array_size)
261+
{
262+
throw invalid_command_line_argument_exceptiont{
263+
"min dynamic array size cannot be greater than max dynamic array size",
264+
"--" FUNCTION_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT
265+
" --" FUNCTION_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT};
266+
}
186267
}
187268

188269
std::size_t function_call_harness_generatort::require_one_size_value(
@@ -265,13 +346,43 @@ function_call_harness_generatort::implt::declare_arguments(
265346
function_to_call.location,
266347
"__goto_harness",
267348
*symbol_table};
349+
std::map<irep_idt, irep_idt> parameter_name_to_argument_name;
268350
for(const auto &parameter : parameters)
269351
{
270352
auto argument = allocate_objects.allocate_automatic_local_object(
271353
parameter.type(), parameter.get_base_name());
354+
parameter_name_to_argument_name.insert(
355+
{parameter.get_base_name(), argument.get_identifier()});
272356
arguments.push_back(argument);
273357
}
274358

359+
for(const auto &p : parameter_name_to_argument_name)
360+
{
361+
auto const &parameter_name = p.first;
362+
auto const &argument_name = p.second;
363+
if(
364+
function_parameters_to_treat_as_arrays.find(parameter_name) !=
365+
function_parameters_to_treat_as_arrays.end())
366+
{
367+
function_arguments_to_treat_as_arrays.insert(argument_name);
368+
}
369+
auto it = function_parameter_to_associated_array_size.find(parameter_name);
370+
if(it != function_parameter_to_associated_array_size.end())
371+
{
372+
auto const &associated_array_size_parameter = it->second;
373+
auto associated_array_size_argument =
374+
parameter_name_to_argument_name.find(associated_array_size_parameter);
375+
if(
376+
associated_array_size_argument == parameter_name_to_argument_name.end())
377+
{
378+
throw invalid_command_line_argument_exceptiont{
379+
"associated array size is not there",
380+
"--" FUNCTION_HARNESS_GENERATOR_ASSOCIATED_ARRAY_SIZE_OPT};
381+
}
382+
function_argument_to_associated_array_size.insert(
383+
{argument_name, associated_array_size_argument->second});
384+
}
385+
}
275386
allocate_objects.declare_created_symbols(function_body);
276387
return arguments;
277388
}

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