Skip to content

Commit f910b7b

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 63ae284 commit f910b7b

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

114114
static abstract_object_sett compact_values(const abstract_object_sett &values);
115+
static abstract_object_sett
116+
non_destructive_compact(const abstract_object_sett &values);
117+
static abstract_object_sett widen_value_set(
118+
const constant_interval_exprt &lhs,
119+
const constant_interval_exprt &rhs);
115120

116121
value_set_abstract_objectt::value_set_abstract_objectt(const typet &type)
117122
: abstract_value_objectt(type)
@@ -212,6 +217,18 @@ abstract_object_pointert value_set_abstract_objectt::merge_with_value(
212217
else
213218
union_values.insert(other);
214219

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

@@ -461,7 +478,7 @@ destructive_compact(abstract_object_sett values, int slice)
461478
auto upper_start = eval_expr(minus_exprt(width.get_upper(), slice_width));
462479
if(
463480
lower_boundary ==
464-
upper_start) // adjust so the intervals are not immediately combined
481+
upper_start) // adjust lower_boundary so the intervals are immediately combined
465482
upper_start = eval_expr(
466483
plus_exprt(upper_start, from_integer(1, lower_boundary.type())));
467484

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

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

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

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

0 commit comments

Comments
 (0)