Skip to content

Commit 39f1987

Browse files
jezhigginsjezhiggins
committed
Widen value_sets by extending boundary values with an interval
If the range of the merged value_set is no wider than the original object, no widening takes place. Otherwise, both the upper and lower boundary value can be extended, if the merged-in value extends in that direction.
1 parent 11e2676 commit 39f1987

File tree

5 files changed

+393
-102
lines changed

5 files changed

+393
-102
lines changed

‎regression/goto-analyzer/loop-termination-ne/test-unwind-5-intervals.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,5 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^main::1::1::i .* \[5, 5\] @ \[6\]
7+
^main::1::p .* \[2, 1F9\] @ \[5\]
78
--

‎regression/goto-analyzer/loop-termination-ne/test-unwind-5-value-sets.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,5 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^main::1::1::i .* value-set-begin: 5 :value-set-end @ \[6\]
7-
^main::1::p .* value-set-begin: 2, 17, 32 :value-set-end @ \[5\]
7+
^main::1::p .* value-set-begin: 2, \[11, 1F9\] :value-set-end @ \[5\]
88
--

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

Lines changed: 57 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,6 +117,11 @@ maybe_extract_single_value(const abstract_object_pointert &maybe_singleton);
117117
static bool are_any_top(const abstract_object_sett &set);
118118

119119
static abstract_object_sett compact_values(const abstract_object_sett &values);
120+
static abstract_object_sett
121+
non_destructive_compact(const abstract_object_sett &values);
122+
static abstract_object_sett widen_value_set(
123+
const constant_interval_exprt &lhs,
124+
const constant_interval_exprt &rhs);
120125

121126
value_set_abstract_objectt::value_set_abstract_objectt(const typet &type)
122127
: abstract_value_objectt(type)
@@ -217,6 +222,18 @@ abstract_object_pointert value_set_abstract_objectt::merge_with_value(
217222
else
218223
union_values.insert(other);
219224

225+
auto has_values = [](const abstract_object_pointert &v) {
226+
return !v->is_top() && !v->is_bottom();
227+
};
228+
229+
if(
230+
widen_mode == widen_modet::could_widen && has_values(shared_from_this()) &&
231+
has_values(other))
232+
{
233+
union_values.insert(widen_value_set(to_interval(), other->to_interval()));
234+
union_values = non_destructive_compact(union_values);
235+
}
236+
220237
return resolve_values(union_values);
221238
}
222239

@@ -490,7 +507,7 @@ destructive_compact(abstract_object_sett values, int slice)
490507
auto upper_start = eval_expr(minus_exprt(width.get_upper(), slice_width));
491508
if(
492509
lower_boundary ==
493-
upper_start) // adjust so the intervals are not immediately combined
510+
upper_start) // adjust boundary so intervals aren't immediately combined
494511
upper_start = eval_expr(
495512
plus_exprt(upper_start, from_integer(1, lower_boundary.type())));
496513

@@ -535,3 +552,42 @@ static bool is_le(const exprt &lhs, const exprt &rhs)
535552
auto is_le_expr = binary_relation_exprt(lhs, ID_le, rhs);
536553
return eval_expr(is_le_expr).is_true();
537554
}
555+
556+
static abstract_object_sett widen_value_set(
557+
const constant_interval_exprt &lhs,
558+
const constant_interval_exprt &rhs)
559+
{
560+
auto widened_ends = abstract_object_sett{};
561+
562+
if(lhs.contains(rhs))
563+
return widened_ends;
564+
565+
auto lower_bound =
566+
constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower());
567+
auto upper_bound =
568+
constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper());
569+
auto range = plus_exprt(
570+
minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
571+
572+
auto symbol_table = symbol_tablet{};
573+
auto ns = namespacet{symbol_table};
574+
575+
// should extend lower bound?
576+
if(rhs.get_lower() < lhs.get_lower())
577+
{
578+
auto widened_lower_bound =
579+
simplify_expr(minus_exprt(lower_bound, range), ns);
580+
widened_ends.insert(interval_abstract_valuet::make_interval(
581+
constant_interval_exprt(widened_lower_bound, lower_bound)));
582+
}
583+
// should extend upper bound?
584+
if(lhs.get_upper() < rhs.get_upper())
585+
{
586+
auto widened_upper_bound =
587+
simplify_expr(plus_exprt(upper_bound, range), ns);
588+
widened_ends.insert(interval_abstract_valuet::make_interval(
589+
constant_interval_exprt(upper_bound, widened_upper_bound)));
590+
}
591+
592+
return widened_ends;
593+
}

‎unit/analyses/variable-sensitivity/interval_abstract_value/widening_merge.cpp

Lines changed: 100 additions & 100 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,106 @@ SCENARIO(
8080
}
8181
}
8282

83+
GIVEN("widening merges with TOP or BOTTOM")
84+
{
85+
WHEN("merging [1, 2] with TOP")
86+
{
87+
auto op1 = make_interval(val1, val2, environment, ns);
88+
auto top2 = make_top_interval();
89+
90+
auto merged = widening_merge(op1, top2);
91+
92+
THEN("result is modified TOP")
93+
{
94+
EXPECT_MODIFIED_TOP(merged);
95+
}
96+
}
97+
WHEN("merging [1, 2] with BOTTOM")
98+
{
99+
auto op1 = make_interval(val1, val2, environment, ns);
100+
auto bottom2 = make_bottom_interval();
101+
102+
auto merged = widening_merge(op1, bottom2);
103+
104+
THEN("result is unmodified [1, 2]")
105+
{
106+
EXPECT_UNMODIFIED(merged, val1, val2);
107+
}
108+
}
109+
WHEN("merging TOP with [1, 2]")
110+
{
111+
auto top1 = make_top_interval();
112+
auto op2 = make_interval(val1, val2, environment, ns);
113+
114+
auto merged = widening_merge(top1, op2);
115+
116+
THEN("result is unmodified TOP")
117+
{
118+
EXPECT_UNMODIFIED_TOP(merged);
119+
}
120+
}
121+
WHEN("merging BOTTOM with [1, 2]")
122+
{
123+
auto bottom1 = make_bottom_interval();
124+
auto op2 = make_interval(val1, val2, environment, ns);
125+
126+
auto merged = widening_merge(bottom1, op2);
127+
128+
THEN("result is modified [1, 2]")
129+
{
130+
EXPECT_MODIFIED(merged, val1, val2);
131+
}
132+
}
133+
WHEN("merging TOP with TOP")
134+
{
135+
auto top1 = make_top_interval();
136+
auto top2 = make_top_interval();
137+
138+
auto merged = widening_merge(top1, top2);
139+
140+
THEN("result is unmodified TOP")
141+
{
142+
EXPECT_UNMODIFIED_TOP(merged);
143+
}
144+
}
145+
WHEN("merging TOP with BOTTOM")
146+
{
147+
auto top1 = make_top_interval();
148+
auto bottom2 = make_bottom_interval();
149+
150+
auto merged = widening_merge(top1, bottom2);
151+
152+
THEN("result is unmodified TOP")
153+
{
154+
EXPECT_UNMODIFIED_TOP(merged);
155+
}
156+
}
157+
WHEN("merging BOTTOM with TOP")
158+
{
159+
auto bottom1 = make_bottom_interval();
160+
auto top2 = make_top_interval();
161+
162+
auto merged = widening_merge(bottom1, top2);
163+
164+
THEN("result is modified TOP")
165+
{
166+
EXPECT_MODIFIED_TOP(merged);
167+
}
168+
}
169+
WHEN("merging BOTTOM with BOTTOM")
170+
{
171+
auto bottom1 = make_bottom_interval();
172+
auto bottom2 = make_bottom_interval();
173+
174+
auto merged = widening_merge(bottom1, bottom2);
175+
176+
THEN("result is unmodified BOTTOM")
177+
{
178+
EXPECT_UNMODIFIED_BOTTOM(merged);
179+
}
180+
}
181+
}
182+
83183
GIVEN("interval merges which do widen")
84184
{
85185
WHEN("merging [1, 3] with [2, 4]")
@@ -203,104 +303,4 @@ SCENARIO(
203303
}
204304
}
205305
}
206-
207-
GIVEN("widening merges with TOP or BOTTOM")
208-
{
209-
WHEN("merging [1, 2] with TOP")
210-
{
211-
auto op1 = make_interval(val1, val2, environment, ns);
212-
auto top2 = make_top_interval();
213-
214-
auto merged = widening_merge(op1, top2);
215-
216-
THEN("result is modified TOP")
217-
{
218-
EXPECT_MODIFIED_TOP(merged);
219-
}
220-
}
221-
WHEN("merging [1, 2] with BOTTOM")
222-
{
223-
auto op1 = make_interval(val1, val2, environment, ns);
224-
auto bottom2 = make_bottom_interval();
225-
226-
auto merged = widening_merge(op1, bottom2);
227-
228-
THEN("result is unmodified [1, 2]")
229-
{
230-
EXPECT_UNMODIFIED(merged, val1, val2);
231-
}
232-
}
233-
WHEN("merging TOP with [1, 2]")
234-
{
235-
auto top1 = make_top_interval();
236-
auto op2 = make_interval(val1, val2, environment, ns);
237-
238-
auto merged = widening_merge(top1, op2);
239-
240-
THEN("result is unmodified TOP")
241-
{
242-
EXPECT_UNMODIFIED_TOP(merged);
243-
}
244-
}
245-
WHEN("merging BOTTOM with [1, 2]")
246-
{
247-
auto bottom1 = make_bottom_interval();
248-
auto op2 = make_interval(val1, val2, environment, ns);
249-
250-
auto merged = widening_merge(bottom1, op2);
251-
252-
THEN("result is modified [1, 2]")
253-
{
254-
EXPECT_MODIFIED(merged, val1, val2);
255-
}
256-
}
257-
WHEN("merging TOP with TOP")
258-
{
259-
auto top1 = make_top_interval();
260-
auto top2 = make_top_interval();
261-
262-
auto merged = widening_merge(top1, top2);
263-
264-
THEN("result is unmodified TOP")
265-
{
266-
EXPECT_UNMODIFIED_TOP(merged);
267-
}
268-
}
269-
WHEN("merging TOP with BOTTOM")
270-
{
271-
auto top1 = make_top_interval();
272-
auto bottom2 = make_bottom_interval();
273-
274-
auto merged = widening_merge(top1, bottom2);
275-
276-
THEN("result is unmodified TOP")
277-
{
278-
EXPECT_UNMODIFIED_TOP(merged);
279-
}
280-
}
281-
WHEN("merging BOTTOM with TOP")
282-
{
283-
auto bottom1 = make_bottom_interval();
284-
auto top2 = make_top_interval();
285-
286-
auto merged = widening_merge(bottom1, top2);
287-
288-
THEN("result is modified TOP")
289-
{
290-
EXPECT_MODIFIED_TOP(merged);
291-
}
292-
}
293-
WHEN("merging BOTTOM with BOTTOM")
294-
{
295-
auto bottom1 = make_bottom_interval();
296-
auto bottom2 = make_bottom_interval();
297-
298-
auto merged = widening_merge(bottom1, bottom2);
299-
300-
THEN("result is unmodified BOTTOM")
301-
{
302-
EXPECT_UNMODIFIED_BOTTOM(merged);
303-
}
304-
}
305-
}
306306
}

0 commit comments

Comments
 (0)