1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
/*******************************************************************\
Module: Unit tests for array pool in
solvers/refinement/string_constraint_generator.h
Author: Diffblue Ltd.
\*******************************************************************/
#include <testing-utils/use_catch.h>
#include <solvers/strings/array_pool.h>
#include <util/pointer_expr.h>
SCENARIO("array_pool", "[core][solvers][strings][string_constraint_generator]")
{
const std::size_t pointer_width = 16;
const auto char_type = unsignedbv_typet(8);
const auto length_type = signedbv_typet(32);
const auto pointer_type = pointer_typet(char_type, pointer_width);
GIVEN("An array pool")
{
symbol_generatort symbol_generator;
array_poolt pool(symbol_generator);
WHEN("Looking for a pointer symbol")
{
const symbol_exprt pointer("my_pointer", pointer_type);
const symbol_exprt pointer_length("my_pointer_length", length_type);
const array_string_exprt associated_array =
pool.find(pointer, pointer_length);
THEN("A second find give the same array")
{
const array_string_exprt second_lookup =
pool.find(pointer, pointer_length);
REQUIRE(second_lookup == associated_array);
}
}
WHEN("Looking for the address of the first element of a constant array")
{
const array_typet array_type(char_type, from_integer(3, length_type));
const array_exprt array(
{from_integer('f', char_type),
from_integer('o', char_type),
from_integer('o', char_type)},
array_type);
const exprt first_element =
index_exprt(array, from_integer(0, length_type));
const exprt pointer = address_of_exprt(first_element, pointer_type);
const array_string_exprt associated_array =
pool.find(pointer, array_type.size());
THEN("The associated array should be the pointed array")
{
REQUIRE(associated_array == array);
}
}
WHEN("Looking for a null pointer")
{
const null_pointer_exprt null_pointer(pointer_type);
const symbol_exprt pointer_length("null_pointer_length", length_type);
const array_string_exprt associated_array =
pool.find(null_pointer, pointer_length);
THEN("`find` always gives the same array")
{
const symbol_exprt pointer_length2("null_pointer_length2", length_type);
const array_string_exprt second_lookup =
pool.find(null_pointer, pointer_length2);
REQUIRE(second_lookup == associated_array);
}
}
WHEN("Looking for an if-expression")
{
const exprt boolean_symbol = symbol_exprt("boolean", bool_typet());
const exprt true_case = symbol_exprt("pointer1", pointer_type);
const exprt false_case = symbol_exprt("pointer2", pointer_type);
const exprt if_expr = if_exprt(boolean_symbol, true_case, false_case);
const symbol_exprt pointer_length("pointer_length", length_type);
const array_string_exprt associated_array =
pool.find(if_expr, pointer_length);
THEN(
"Arrays associated to the subexpressions are the subexpressions of "
"the associated array")
{
const symbol_exprt pointer_length1("pointer_length1", length_type);
const array_string_exprt associated_to_true =
pool.find(true_case, pointer_length1);
const symbol_exprt pointer_length2("pointer_length2", length_type);
const array_string_exprt associated_to_false =
pool.find(false_case, pointer_length2);
const typet recomposed_type = array_typet(
char_type, if_exprt(boolean_symbol, pointer_length, pointer_length));
const exprt recomposed_array = if_exprt(
boolean_symbol,
associated_to_true,
associated_to_false,
recomposed_type);
REQUIRE(associated_array == recomposed_array);
}
}
WHEN("Looking for two pointer symbols")
{
const exprt true_case = symbol_exprt("pointer1", pointer_type);
const symbol_exprt pointer_length1("pointer_length1", length_type);
const exprt false_case = symbol_exprt("pointer2", pointer_type);
const symbol_exprt pointer_length2("pointer_length2", length_type);
const array_string_exprt associated_to_true =
pool.find(true_case, pointer_length1);
const array_string_exprt associated_to_false =
pool.find(false_case, pointer_length2);
THEN("Looking for an if-expression containing these two symbols")
{
const exprt boolean_symbol = symbol_exprt("boolean", bool_typet());
const exprt if_expr = if_exprt(boolean_symbol, true_case, false_case);
const symbol_exprt pointer_length("pointer_length", length_type);
const array_string_exprt associated_array =
pool.find(if_expr, pointer_length);
const typet recomposed_type = array_typet(
char_type,
if_exprt(boolean_symbol, pointer_length1, pointer_length2));
const exprt recomposed_array = if_exprt(
boolean_symbol,
associated_to_true,
associated_to_false,
recomposed_type);
REQUIRE(associated_array == recomposed_array);
}
}
}
}
|
