Skip to content

Commit 82aa431

Browse files
jezhigginsjezhiggins
committed
Add vsd_configt::maximum_array_index, pick up in full_array_abstract_object
1 parent 341fae5 commit 82aa431

File tree

3 files changed

+121
-103
lines changed

3 files changed

+121
-103
lines changed

‎src/analyses/variable-sensitivity/full_array_abstract_object.cpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
#include <ostream>
1010

1111
#include <analyses/variable-sensitivity/abstract_environment.h>
12+
#include <analyses/variable-sensitivity/variable_sensitivity_configuration.h>
1213
#include <util/arith_tools.h>
1314
#include <util/mathematical_types.h>
1415
#include <util/std_expr.h>
@@ -25,8 +26,6 @@ struct eval_index_resultt
2526
bool overrun;
2627
};
2728

28-
static mp_integer max_array_index = 10;
29-
3029
static eval_index_resultt eval_index(
3130
const exprt &expr,
3231
const abstract_environmentt &env,
@@ -469,6 +468,7 @@ static eval_index_resultt eval_index(
469468
mp_integer out_index;
470469
bool result = to_integer(to_constant_expr(value), out_index);
471470

471+
auto max_array_index = env.configuration().maximum_array_index;
472472
bool overrun = (out_index > max_array_index);
473473

474474
return {!result, overrun ? max_array_index : out_index, overrun};

‎src/analyses/variable-sensitivity/variable_sensitivity_configuration.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@
1111
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H
1212
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_CONFIGURATION_H
1313

14+
#include <limits>
1415
#include <map>
1516

1617
#include <util/exception_utils.h>
@@ -51,6 +52,8 @@ struct vsd_configt
5152

5253
flow_sensitivityt flow_sensitivity;
5354

55+
size_t maximum_array_index = std::numeric_limits<size_t>::max();
56+
5457
struct
5558
{
5659
bool liveness;

‎unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp‎

Lines changed: 116 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -39,122 +39,137 @@ SCENARIO(
3939
"[core][analyses][variable-sensitivity][full_array_abstract_object][max_"
4040
"array]")
4141
{
42-
auto object_factory = variable_sensitivity_object_factoryt::configured_with(
43-
vsd_configt::value_set());
44-
abstract_environmentt environment(object_factory);
45-
environment.make_top();
46-
symbol_tablet symbol_table;
47-
namespacet ns(symbol_table);
48-
49-
WHEN("array = {1, 2, 3}, writes under maximum size")
42+
for(size_t max_array_index = 10; max_array_index <= 20; max_array_index += 10)
5043
{
51-
WHEN("array[3] = 4")
44+
auto configuration = vsd_configt::value_set();
45+
configuration.maximum_array_index = max_array_index;
46+
47+
auto object_factory =
48+
variable_sensitivity_object_factoryt::configured_with(configuration);
49+
abstract_environmentt environment(object_factory);
50+
environment.make_top();
51+
symbol_tablet symbol_table;
52+
namespacet ns(symbol_table);
53+
WHEN("maximum size is " + std::to_string(max_array_index))
5254
{
53-
auto array = build_array({1, 2, 3}, environment, ns);
54-
55-
auto updated = write_array(array, 3, 4, environment, ns);
56-
57-
THEN("array equals {1, 2, 3, 4}")
55+
WHEN("array = {1, 2, 3}, writes under maximum size")
5856
{
59-
EXPECT_INDEX(updated, 0, 1, environment, ns);
60-
EXPECT_INDEX(updated, 1, 2, environment, ns);
61-
EXPECT_INDEX(updated, 2, 3, environment, ns);
62-
EXPECT_INDEX(updated, 3, 4, environment, ns);
63-
}
64-
}
65-
WHEN("a[0] = 99")
66-
{
67-
auto array = build_array({1, 2, 3}, environment, ns);
57+
WHEN("array[3] = 4")
58+
{
59+
auto array = build_array({1, 2, 3}, environment, ns);
6860

69-
auto updated = write_array(array, 0, 99, environment, ns);
61+
auto updated = write_array(array, 3, 4, environment, ns);
7062

71-
THEN("array equals {99, 2, 3}")
72-
{
73-
EXPECT_INDEX(updated, 0, 99, environment, ns);
74-
EXPECT_INDEX(updated, 1, 2, environment, ns);
75-
EXPECT_INDEX(updated, 2, 3, environment, ns);
76-
}
77-
}
78-
WHEN("a[5] = 99")
79-
{
80-
auto array = build_array({1, 2, 3}, environment, ns);
63+
THEN("array equals {1, 2, 3, 4}")
64+
{
65+
EXPECT_INDEX(updated, 0, 1, environment, ns);
66+
EXPECT_INDEX(updated, 1, 2, environment, ns);
67+
EXPECT_INDEX(updated, 2, 3, environment, ns);
68+
EXPECT_INDEX(updated, 3, 4, environment, ns);
69+
}
70+
}
71+
WHEN("a[0] = 99")
72+
{
73+
auto array = build_array({1, 2, 3}, environment, ns);
8174

82-
auto updated = write_array(array, 5, 99, environment, ns);
75+
auto updated = write_array(array, 0, 99, environment, ns);
8376

84-
THEN("array equals {1, 2, 3, <empty>, <empty>, 99}")
85-
{
86-
EXPECT_INDEX(updated, 0, 1, environment, ns);
87-
EXPECT_INDEX(updated, 1, 2, environment, ns);
88-
EXPECT_INDEX(updated, 2, 3, environment, ns);
89-
EXPECT_INDEX_TOP(updated, 3, environment, ns);
90-
EXPECT_INDEX_TOP(updated, 4, environment, ns);
91-
EXPECT_INDEX(updated, 5, 99, environment, ns);
77+
THEN("array equals {99, 2, 3}")
78+
{
79+
EXPECT_INDEX(updated, 0, 99, environment, ns);
80+
EXPECT_INDEX(updated, 1, 2, environment, ns);
81+
EXPECT_INDEX(updated, 2, 3, environment, ns);
82+
}
83+
}
84+
WHEN("a[5] = 99")
85+
{
86+
auto array = build_array({1, 2, 3}, environment, ns);
87+
88+
auto updated = write_array(array, 5, 99, environment, ns);
89+
90+
THEN("array equals {1, 2, 3, <empty>, <empty>, 99}")
91+
{
92+
EXPECT_INDEX(updated, 0, 1, environment, ns);
93+
EXPECT_INDEX(updated, 1, 2, environment, ns);
94+
EXPECT_INDEX(updated, 2, 3, environment, ns);
95+
EXPECT_INDEX_TOP(updated, 3, environment, ns);
96+
EXPECT_INDEX_TOP(updated, 4, environment, ns);
97+
EXPECT_INDEX(updated, 5, 99, environment, ns);
98+
}
99+
}
92100
}
93-
}
94-
}
95-
WHEN("array = {1, 2, 3}, writes beyond maximum size mapped to max_size")
96-
{
97-
WHEN("array[99] = 4")
98-
{
99-
auto array = build_array({1, 2, 3}, environment, ns);
100-
101-
auto updated = write_array(array, 99, 4, environment, ns);
102-
103-
THEN("array equals {1, 2, 3, ..., [10] = 4}")
101+
WHEN("array = {1, 2, 3}, writes beyond maximum size mapped to max_size")
104102
{
105-
EXPECT_INDEX(updated, 0, 1, environment, ns);
106-
EXPECT_INDEX(updated, 1, 2, environment, ns);
107-
EXPECT_INDEX(updated, 2, 3, environment, ns);
108-
EXPECT_INDEX(updated, 10, 4, environment, ns);
109-
}
110-
}
111-
}
112-
WHEN("array = {1, 2, 3}, reads beyond maximum size mapped to max_size")
113-
{
114-
WHEN("a[max] = 4")
115-
{
116-
auto array = build_array({1, 2, 3}, environment, ns);
117-
118-
auto updated = write_array(array, 99, 4, environment, ns);
119-
120-
for(int i = 10; i <= 30; i += 5)
121-
THEN("array[" + std::to_string(i) + "] = 4}")
103+
WHEN("array[99] = 4")
122104
{
123-
EXPECT_INDEX(updated, i, 4, environment, ns);
105+
auto array = build_array({1, 2, 3}, environment, ns);
106+
107+
auto updated = write_array(array, 99, 4, environment, ns);
108+
109+
THEN(
110+
"array equals {1, 2, 3, ..., [" + std::to_string(max_array_index) +
111+
"] = 4}")
112+
{
113+
EXPECT_INDEX(updated, 0, 1, environment, ns);
114+
EXPECT_INDEX(updated, 1, 2, environment, ns);
115+
EXPECT_INDEX(updated, 2, 3, environment, ns);
116+
EXPECT_INDEX(updated, max_array_index, 4, environment, ns);
117+
}
124118
}
125-
}
126-
}
127-
WHEN("array = {1, 2, 3}, writes beyond maximum size are merged")
128-
{
129-
WHEN("array[98] = 3, array[99] = 4")
130-
{
131-
auto array = build_array({1, 2, 3}, environment, ns);
132-
133-
auto updated = write_array(array, 99, 4, environment, ns);
134-
updated = write_array(updated, 98, 3, environment, ns);
135-
136-
THEN("array equals {1, 2, 3, ..., [10] = TOP}")
137-
{
138-
EXPECT_INDEX(updated, 0, 1, environment, ns);
139-
EXPECT_INDEX(updated, 1, 2, environment, ns);
140-
EXPECT_INDEX(updated, 2, 3, environment, ns);
141-
EXPECT_INDEX(updated, 10, {3, 4}, environment, ns);
142119
}
143-
}
144-
WHEN("array[99] = 3, array[99] = 4, array[100] = 5")
145-
{
146-
auto array = build_array({1, 2, 3}, environment, ns);
120+
WHEN("array = {1, 2, 3}, reads beyond maximum size mapped to max_size")
121+
{
122+
WHEN("a[max] = 4")
123+
{
124+
auto array = build_array({1, 2, 3}, environment, ns);
147125

148-
auto updated = write_array(array, 100, 5, environment, ns);
149-
updated = write_array(updated, 99, 4, environment, ns);
150-
updated = write_array(updated, 98, 3, environment, ns);
126+
auto updated =
127+
write_array(array, max_array_index, 4, environment, ns);
151128

152-
THEN("array equals {1, 2, 3, ..., [10] = TOP}")
129+
for(size_t i = max_array_index; i <= max_array_index * 3; i += 5)
130+
THEN("array[" + std::to_string(i) + "] = 4}")
131+
{
132+
EXPECT_INDEX(updated, i, 4, environment, ns);
133+
}
134+
}
135+
}
136+
WHEN("array = {1, 2, 3}, writes beyond maximum size are merged")
153137
{
154-
EXPECT_INDEX(updated, 0, 1, environment, ns);
155-
EXPECT_INDEX(updated, 1, 2, environment, ns);
156-
EXPECT_INDEX(updated, 2, 3, environment, ns);
157-
EXPECT_INDEX(updated, 10, {3, 4, 5}, environment, ns);
138+
WHEN("array[98] = 3, array[99] = 4")
139+
{
140+
auto array = build_array({1, 2, 3}, environment, ns);
141+
142+
auto updated = write_array(array, 99, 4, environment, ns);
143+
updated = write_array(updated, 98, 3, environment, ns);
144+
145+
THEN(
146+
"array equals {1, 2, 3, ..., [" + std::to_string(max_array_index) +
147+
"] = TOP}")
148+
{
149+
EXPECT_INDEX(updated, 0, 1, environment, ns);
150+
EXPECT_INDEX(updated, 1, 2, environment, ns);
151+
EXPECT_INDEX(updated, 2, 3, environment, ns);
152+
EXPECT_INDEX(updated, max_array_index, {3, 4}, environment, ns);
153+
}
154+
}
155+
WHEN("array[99] = 3, array[99] = 4, array[100] = 5")
156+
{
157+
auto array = build_array({1, 2, 3}, environment, ns);
158+
159+
auto updated = write_array(array, 100, 5, environment, ns);
160+
updated = write_array(updated, 99, 4, environment, ns);
161+
updated = write_array(updated, 98, 3, environment, ns);
162+
163+
THEN(
164+
"array equals {1, 2, 3, ..., [" + std::to_string(max_array_index) +
165+
"] = TOP}")
166+
{
167+
EXPECT_INDEX(updated, 0, 1, environment, ns);
168+
EXPECT_INDEX(updated, 1, 2, environment, ns);
169+
EXPECT_INDEX(updated, 2, 3, environment, ns);
170+
EXPECT_INDEX(updated, max_array_index, {3, 4, 5}, environment, ns);
171+
}
172+
}
158173
}
159174
}
160175
}

0 commit comments

Comments
 (0)