Skip to content

Commit ff93829

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 e910e9f commit ff93829

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
@@ -114,6 +114,11 @@ maybe_extract_single_value(const abstract_object_pointert &maybe_singleton);
114114
static bool are_any_top(const abstract_object_sett &set);
115115

116116
static abstract_object_sett compact_values(const abstract_object_sett &values);
117+
static abstract_object_sett
118+
non_destructive_compact(const abstract_object_sett &values);
119+
static abstract_object_sett widen_value_set(
120+
const constant_interval_exprt &lhs,
121+
const constant_interval_exprt &rhs);
117122

118123
value_set_abstract_objectt::value_set_abstract_objectt(const typet &type)
119124
: abstract_value_objectt(type)
@@ -214,6 +219,18 @@ abstract_object_pointert value_set_abstract_objectt::merge_with_value(
214219
else
215220
union_values.insert(other);
216221

222+
auto has_values = [](const abstract_object_pointert &v) {
223+
return !v->is_top() && !v->is_bottom();
224+
};
225+
226+
if(
227+
widen_mode == widen_modet::could_widen && has_values(shared_from_this()) &&
228+
has_values(other))
229+
{
230+
union_values.insert(widen_value_set(to_interval(), other->to_interval()));
231+
union_values = non_destructive_compact(union_values);
232+
}
233+
217234
return resolve_values(union_values);
218235
}
219236

@@ -463,7 +480,7 @@ destructive_compact(abstract_object_sett values, int slice)
463480
auto upper_start = eval_expr(minus_exprt(width.get_upper(), slice_width));
464481
if(
465482
lower_boundary ==
466-
upper_start) // adjust so the intervals are not immediately combined
483+
upper_start) // adjust boundary so intervals aren't immediately combined
467484
upper_start = eval_expr(
468485
plus_exprt(upper_start, from_integer(1, lower_boundary.type())));
469486

@@ -508,3 +525,42 @@ static bool is_le(const exprt &lhs, const exprt &rhs)
508525
auto is_le_expr = binary_relation_exprt(lhs, ID_le, rhs);
509526
return eval_expr(is_le_expr).is_true();
510527
}
528+
529+
static abstract_object_sett widen_value_set(
530+
const constant_interval_exprt &lhs,
531+
const constant_interval_exprt &rhs)
532+
{
533+
auto widened_ends = abstract_object_sett{};
534+
535+
if(lhs.contains(rhs))
536+
return widened_ends;
537+
538+
auto lower_bound =
539+
constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower());
540+
auto upper_bound =
541+
constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper());
542+
auto range = plus_exprt(
543+
minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
544+
545+
auto symbol_table = symbol_tablet{};
546+
auto ns = namespacet{symbol_table};
547+
548+
// should extend lower bound?
549+
if(rhs.get_lower() < lhs.get_lower())
550+
{
551+
auto widened_lower_bound =
552+
simplify_expr(minus_exprt(lower_bound, range), ns);
553+
widened_ends.insert(interval_abstract_valuet::make_interval(
554+
constant_interval_exprt(widened_lower_bound, lower_bound)));
555+
}
556+
// should extend upper bound?
557+
if(lhs.get_upper() < rhs.get_upper())
558+
{
559+
auto widened_upper_bound =
560+
simplify_expr(plus_exprt(upper_bound, range), ns);
561+
widened_ends.insert(interval_abstract_valuet::make_interval(
562+
constant_interval_exprt(upper_bound, widened_upper_bound)));
563+
}
564+
565+
return widened_ends;
566+
}

‎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)