Skip to content

Commit 26b70ff

Browse files
jezhigginsjezhiggins
committed
merge writes beyond array maximum length
1 parent 0a51ed4 commit 26b70ff

File tree

6 files changed

+116
-29
lines changed

6 files changed

+116
-29
lines changed

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

Lines changed: 20 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ struct eval_index_resultt
2222
{
2323
bool is_good;
2424
mp_integer value;
25+
bool overrun;
2526
};
2627

2728
static mp_integer max_array_index = 10;
@@ -275,7 +276,8 @@ abstract_object_pointert full_array_abstract_objectt::write_sub_element(
275276
auto const existing_value = map_find_or_top(index.value, environment, ns);
276277
result->map_put(
277278
index.value,
278-
environment.write(existing_value, value, stack, ns, merging_write));
279+
environment.write(existing_value, value, stack, ns, merging_write),
280+
index.overrun);
279281
result->set_not_top();
280282
DATA_INVARIANT(result->verify(), "Structural invariants maintained");
281283
return result;
@@ -337,7 +339,7 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element(
337339
}
338340
else
339341
{
340-
result->map_put(index.value, value);
342+
result->map_put(index.value, value, index.overrun);
341343
result->set_not_top();
342344

343345
DATA_INVARIANT(result->verify(), "Structural invariants maintained");
@@ -353,14 +355,24 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element(
353355

354356
void full_array_abstract_objectt::map_put(
355357
mp_integer index_value,
356-
const abstract_object_pointert &value)
358+
const abstract_object_pointert &value,
359+
bool overrun)
357360
{
358361
auto old_value = map.find(index_value);
359362

360-
if(old_value.has_value())
361-
map.replace(index_value, value);
362-
else
363+
if(!old_value.has_value())
363364
map.insert(index_value, value);
365+
else
366+
{
367+
// if we're over the max_index, merge with existing value
368+
auto replacement_value =
369+
overrun
370+
? abstract_objectt::merge(old_value.value(), value, widen_modet::no)
371+
.object
372+
: value;
373+
374+
map.replace(index_value, replacement_value);
375+
}
364376
}
365377

366378
abstract_object_pointert full_array_abstract_objectt::map_find_or_top(
@@ -455,8 +467,7 @@ static eval_index_resultt eval_index(
455467
mp_integer out_index;
456468
bool result = to_integer(to_constant_expr(value), out_index);
457469

458-
if(out_index > max_array_index)
459-
out_index = max_array_index;
470+
bool overrun = (out_index > max_array_index);
460471

461-
return {!result, out_index};
472+
return {!result, overrun ? max_array_index : out_index, overrun};
462473
}

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -203,7 +203,10 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt<
203203

204204
shared_array_mapt map;
205205

206-
void map_put(mp_integer index, const abstract_object_pointert &value);
206+
void map_put(
207+
mp_integer index,
208+
const abstract_object_pointert &value,
209+
bool overrun);
207210
abstract_object_pointert map_find_or_top(
208211
mp_integer index,
209212
const abstract_environmentt &env,

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

Lines changed: 51 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -86,8 +86,8 @@ SCENARIO(
8686
EXPECT_INDEX(updated, 0, 1, environment, ns);
8787
EXPECT_INDEX(updated, 1, 2, environment, ns);
8888
EXPECT_INDEX(updated, 2, 3, environment, ns);
89-
EXPECT_EMPTY_INDEX(updated, 3, environment, ns);
90-
EXPECT_EMPTY_INDEX(updated, 4, environment, ns);
89+
EXPECT_INDEX_TOP(updated, 3, environment, ns);
90+
EXPECT_INDEX_TOP(updated, 4, environment, ns);
9191
EXPECT_INDEX(updated, 5, 99, environment, ns);
9292
}
9393
}
@@ -109,4 +109,53 @@ SCENARIO(
109109
}
110110
}
111111
}
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}")
122+
{
123+
EXPECT_INDEX(updated, i, 4, environment, ns);
124+
}
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);
142+
}
143+
}
144+
WHEN("array[99] = 3, array[99] = 4, array[100] = 5")
145+
{
146+
auto array = build_array({1, 2, 3}, environment, ns);
147+
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);
151+
152+
THEN("array equals {1, 2, 3, ..., [10] = TOP}")
153+
{
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);
158+
}
159+
}
160+
}
112161
}

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -84,8 +84,8 @@ SCENARIO(
8484
REQUIRE_FALSE(result.object->is_top());
8585
REQUIRE_FALSE(result.object->is_bottom());
8686
EXPECT_INDEX(result.object, 0, val1[0], environment, ns);
87-
EXPECT_EMPTY_INDEX(result.object, 1, environment, ns);
88-
EXPECT_EMPTY_INDEX(result.object, 1, environment, ns);
87+
EXPECT_INDEX_TOP(result.object, 1, environment, ns);
88+
EXPECT_INDEX_TOP(result.object, 1, environment, ns);
8989

9090
// Since it has modified, we definitely shouldn't be reusing the pointer
9191
REQUIRE_FALSE(result.object == op1);
@@ -107,7 +107,7 @@ SCENARIO(
107107
REQUIRE(result.object->is_top());
108108
REQUIRE_FALSE(result.object->is_bottom());
109109
for(int i = 0; i != 3; ++i)
110-
EXPECT_EMPTY_INDEX(result.object, i, environment, ns);
110+
EXPECT_INDEX_TOP(result.object, i, environment, ns);
111111

112112
// We can't reuse the abstract object as the value has changed
113113
REQUIRE(result.object != op1);
@@ -151,7 +151,7 @@ SCENARIO(
151151
REQUIRE(result.object->is_top());
152152
REQUIRE_FALSE(result.object->is_bottom());
153153
for(int i = 0; i != 3; ++i)
154-
EXPECT_EMPTY_INDEX(result.object, i, environment, ns);
154+
EXPECT_INDEX_TOP(result.object, i, environment, ns);
155155

156156
// Is optimal
157157
REQUIRE(result.object == op1);
@@ -173,7 +173,7 @@ SCENARIO(
173173
REQUIRE(result.object->is_top());
174174
REQUIRE_FALSE(result.object->is_bottom());
175175
for(int i = 0; i != 3; ++i)
176-
EXPECT_EMPTY_INDEX(result.object, i, environment, ns);
176+
EXPECT_INDEX_TOP(result.object, i, environment, ns);
177177

178178
// Is optimal
179179
REQUIRE(result.object == op1);
@@ -195,7 +195,7 @@ SCENARIO(
195195
REQUIRE(result.object->is_top());
196196
REQUIRE_FALSE(result.object->is_bottom());
197197
for(int i = 0; i != 3; ++i)
198-
EXPECT_EMPTY_INDEX(result.object, i, environment, ns);
198+
EXPECT_INDEX_TOP(result.object, i, environment, ns);
199199

200200
// Is optimal
201201
REQUIRE(result.object == op1);
@@ -239,7 +239,7 @@ SCENARIO(
239239
REQUIRE(result.object->is_top());
240240
REQUIRE_FALSE(result.object->is_bottom());
241241
for(int i = 0; i != 3; ++i)
242-
EXPECT_EMPTY_INDEX(result.object, i, environment, ns);
242+
EXPECT_INDEX_TOP(result.object, i, environment, ns);
243243

244244
// Is optimal
245245
REQUIRE(result.object != op1);

‎unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp

Lines changed: 27 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,8 @@ as_interval(const abstract_object_pointert &aop)
140140
std::shared_ptr<const value_set_abstract_objectt>
141141
as_value_set(const abstract_object_pointert &aop)
142142
{
143-
return std::dynamic_pointer_cast<const value_set_abstract_objectt>(aop);
143+
return std::dynamic_pointer_cast<const value_set_abstract_objectt>(
144+
aop->unwrap_context());
144145
}
145146

146147
bool set_contains(const std::vector<exprt> &set, const exprt &val)
@@ -272,10 +273,7 @@ void EXPECT(
272273
REQUIRE(values.size() == expected_values.size());
273274

274275
for(auto &ev : expected_values)
275-
{
276-
INFO("Expect " + value_string + " to match " + expected_string);
277276
REQUIRE(set_contains(values, ev));
278-
}
279277
}
280278

281279
void EXPECT(
@@ -313,19 +311,39 @@ void EXPECT_INDEX(
313311
REQUIRE(expr_to_str(expr) == expr_to_str(expected_expr));
314312
}
315313

316-
void EXPECT_EMPTY_INDEX(
314+
void EXPECT_INDEX(
317315
std::shared_ptr<const abstract_objectt> &result,
318316
int index,
317+
std::vector<int> expected,
319318
abstract_environmentt &environment,
320319
namespacet &ns)
321320
{
322321
auto type = signedbv_typet(32);
323322
auto index_expr = index_exprt(nil_exprt(), from_integer(index, type));
324-
auto expr = result->expression_transform(index_expr, {}, environment, ns)
325-
->to_constant();
323+
auto value =
324+
as_value_set(result->expression_transform(index_expr, {}, environment, ns));
325+
326+
auto expected_exprs = std::vector<exprt>{};
327+
for(int e : expected)
328+
expected_exprs.push_back(from_integer(e, type));
329+
INFO(
330+
"Expect array[" + std::to_string(index) +
331+
"] == " + exprs_to_str(expected_exprs));
332+
EXPECT(value, expected_exprs);
333+
}
334+
335+
void EXPECT_INDEX_TOP(
336+
std::shared_ptr<const abstract_objectt> &result,
337+
int index,
338+
abstract_environmentt &environment,
339+
namespacet &ns)
340+
{
341+
auto type = signedbv_typet(32);
342+
auto index_expr = index_exprt(nil_exprt(), from_integer(index, type));
343+
auto value = result->expression_transform(index_expr, {}, environment, ns);
326344

327-
INFO("Expect array[" + std::to_string(index) + "] to be empty");
328-
REQUIRE(expr_to_str(expr) == expr_to_str(nil_exprt()));
345+
INFO("Expect array[" + std::to_string(index) + "] to be TOP");
346+
REQUIRE(value->is_top());
329347
}
330348

331349
void EXPECT_UNMODIFIED(

‎unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,7 +90,13 @@ void EXPECT_INDEX(
9090
int expected,
9191
abstract_environmentt &environment,
9292
namespacet &ns);
93-
void EXPECT_EMPTY_INDEX(
93+
void EXPECT_INDEX(
94+
std::shared_ptr<const abstract_objectt> &result,
95+
int index,
96+
std::vector<int> expected,
97+
abstract_environmentt &environment,
98+
namespacet &ns);
99+
void EXPECT_INDEX_TOP(
94100
std::shared_ptr<const abstract_objectt> &result,
95101
int index,
96102
abstract_environmentt &environment,

0 commit comments

Comments
 (0)