Skip to content

Commit 714cee3

Browse files
committed
Correct value_set merge implementation.
Ensure bottom flag is cleared when returning a new object. Intervals and constants can be merged into the a set. Extend abstract_object_set to_interval to handle intervals in the set
1 parent 249ca30 commit 714cee3

File tree

10 files changed

+342
-140
lines changed

10 files changed

+342
-140
lines changed

src/analyses/variable-sensitivity/abstract_object.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -456,6 +456,10 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
456456
top = false;
457457
this->set_not_top_internal();
458458
}
459+
void set_not_bottom()
460+
{
461+
bottom = false;
462+
}
459463
};
460464

461465
struct abstract_hashert

src/analyses/variable-sensitivity/abstract_object_set.cpp

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -41,13 +41,20 @@ constant_interval_exprt abstract_object_sett::to_interval() const
4141
{
4242
PRECONDITION(!values.empty());
4343

44-
exprt lower_expr = first()->to_constant();
45-
exprt upper_expr = first()->to_constant();
44+
const auto &initial =
45+
std::dynamic_pointer_cast<const abstract_value_objectt>(first());
46+
47+
exprt lower_expr = initial->to_interval().get_lower();
48+
exprt upper_expr = initial->to_interval().get_upper();
4649
for(const auto &value : values)
4750
{
48-
const auto &value_expr = value->to_constant();
49-
lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr);
50-
upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr);
51+
const auto &v =
52+
std::dynamic_pointer_cast<const abstract_value_objectt>(value);
53+
const auto &value_expr = v->to_interval();
54+
lower_expr =
55+
constant_interval_exprt::get_min(lower_expr, value_expr.get_lower());
56+
upper_expr =
57+
constant_interval_exprt::get_max(upper_expr, value_expr.get_upper());
5158
}
5259
return constant_interval_exprt(lower_expr, upper_expr);
5360
}

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -229,19 +229,19 @@ abstract_object_pointert value_set_abstract_objectt::resolve_values(
229229
abstract_object_pointert
230230
value_set_abstract_objectt::merge(abstract_object_pointert other) const
231231
{
232+
auto union_values = !is_bottom() ? values : abstract_object_sett{};
233+
232234
auto other_value_set = std::dynamic_pointer_cast<const value_set_tag>(other);
233235
if(other_value_set)
234236
{
235-
auto union_values = values;
236237
union_values.insert(other_value_set->get_values());
237238
return resolve_values(union_values);
238239
}
239240

240241
auto other_value =
241-
std::dynamic_pointer_cast<const constant_abstract_valuet>(other);
242+
std::dynamic_pointer_cast<const abstract_value_objectt>(other);
242243
if(other_value)
243244
{
244-
auto union_values = values;
245245
union_values.insert(other_value);
246246
return resolve_values(union_values);
247247
}
@@ -268,6 +268,7 @@ void value_set_abstract_objectt::set_values(
268268
set_not_top();
269269
values = other_values;
270270
}
271+
set_not_bottom();
271272
verify();
272273
}
273274

unit/analyses/variable-sensitivity/interval_abstract_value/merge.cpp

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -453,6 +453,32 @@ SCENARIO(
453453
EXPECT_MODIFIED(merged, val1, val4);
454454
}
455455
}
456+
WHEN("merging [3, 4] with { [4, 6] }")
457+
{
458+
auto op1 = make_interval(val3, val4, environment, ns);
459+
auto op2 =
460+
make_value_set({constant_interval_exprt(val4, val6)}, environment, ns);
461+
462+
auto merged = merge(op1, op2);
463+
464+
THEN("result is modified [3, 6]")
465+
{
466+
EXPECT_MODIFIED(merged, val3, val6);
467+
}
468+
}
469+
WHEN("merging [3, 4] with { 1, [3, 3] }")
470+
{
471+
auto op1 = make_interval(val3, val4, environment, ns);
472+
auto op2 = make_value_set(
473+
{val1, constant_interval_exprt(val3, val3)}, environment, ns);
474+
475+
auto merged = merge(op1, op2);
476+
477+
THEN("result is modified [1, 4]")
478+
{
479+
EXPECT_MODIFIED(merged, val1, val4);
480+
}
481+
}
456482
WHEN("merging BOTTOM with { 3 }")
457483
{
458484
auto op1 = make_bottom_interval();
@@ -478,4 +504,4 @@ SCENARIO(
478504
}
479505
}
480506
}
481-
}
507+
}
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
analyses
22
testing-utils
3+
util
34

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
analyses
2+
testing-utils
3+
util

0 commit comments

Comments
 (0)