Skip to content

Commit fd01ee8

Browse files
committed
Two phase destructive compact
If added intervals don't reduce the size of the set, widen intervals towards the middle of the range, and repeat.
1 parent 164468e commit fd01ee8

File tree

2 files changed

+61
-25
lines changed

2 files changed

+61
-25
lines changed

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

Lines changed: 11 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -348,7 +348,8 @@ static bool are_any_top(const abstract_object_sett &set)
348348
/////////////////
349349
static abstract_object_sett
350350
non_destructive_compact(const abstract_object_sett &values);
351-
static abstract_object_sett destructive_compact(abstract_object_sett values);
351+
static abstract_object_sett
352+
destructive_compact(abstract_object_sett values, int slice = 3);
352353
static bool value_is_not_contained_in(
353354
const abstract_object_pointert &object,
354355
const std::vector<constant_interval_exprt> &intervals);
@@ -405,12 +406,14 @@ exprt eval_expr(exprt e)
405406
return simplify_expr(e, dummy_namespace);
406407
}
407408

408-
static abstract_object_sett destructive_compact(abstract_object_sett values)
409+
static abstract_object_sett
410+
destructive_compact(abstract_object_sett values, int slice)
409411
{
412+
auto value_count = values.size();
410413
auto width = values.to_interval();
411414
auto slice_width = eval_expr(div_exprt(
412415
minus_exprt(width.get_upper(), width.get_lower()),
413-
from_integer(3, width.type())));
416+
from_integer(slice, width.type())));
414417

415418
auto lower_slice = constant_interval_exprt(
416419
width.get_lower(), eval_expr(plus_exprt(width.get_lower(), slice_width)));
@@ -420,7 +423,11 @@ static abstract_object_sett destructive_compact(abstract_object_sett values)
420423
values.insert(interval_abstract_valuet::make_interval(lower_slice));
421424
values.insert(interval_abstract_valuet::make_interval(upper_slice));
422425

423-
return non_destructive_compact(values);
426+
auto compacted = non_destructive_compact(values);
427+
if(compacted.size() == value_count)
428+
return destructive_compact(compacted, --slice);
429+
430+
return compacted;
424431
} // destructive_compact
425432

426433
static bool value_is_not_contained_in(

unit/analyses/variable-sensitivity/value_set_abstract_object/compacting.cpp

Lines changed: 50 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,15 @@
44
55
Compacting occurs when the value_set get 'large', and takes two forms
66
non-destructive (eg, can we merge constants into an existing interval
7-
with no loss of precision) and desctructive (creating intervals from
7+
with no loss of precision) and destructive (creating intervals from
88
the constants, or merging existing intervals).
99
1010
Author: Jez Higgins, [email protected]
1111
1212
\*******************************************************************/
1313

14-
#include "../variable_sensitivity_test_helpers.h"
15-
1614
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
15+
#include <analyses/variable-sensitivity/variable_sensitivity_test_helpers.h>
1716

1817
#include <testing-utils/use_catch.h>
1918

@@ -26,20 +25,21 @@ SCENARIO(
2625
"[core][analysis][variable-sensitivity][value_set_abstract_object][compact]")
2726
{
2827
const typet type = signedbv_typet(32);
29-
const exprt val1 = from_integer(1, type);
30-
const exprt val2 = from_integer(2, type);
31-
const exprt val3 = from_integer(3, type);
32-
const exprt val4 = from_integer(4, type);
33-
const exprt val5 = from_integer(5, type);
34-
const exprt val6 = from_integer(6, type);
35-
const exprt val7 = from_integer(7, type);
36-
const exprt val8 = from_integer(8, type);
37-
const exprt val9 = from_integer(9, type);
38-
const exprt val10 = from_integer(10, type);
39-
const exprt val11 = from_integer(11, type);
40-
const exprt val12 = from_integer(12, type);
41-
const exprt interval_5_10 = constant_interval_exprt(val5, val10);
42-
const exprt interval_1_10 = constant_interval_exprt(val1, val10);
28+
auto val0 = from_integer(0, type);
29+
auto val1 = from_integer(1, type);
30+
auto val2 = from_integer(2, type);
31+
auto val3 = from_integer(3, type);
32+
auto val4 = from_integer(4, type);
33+
auto val5 = from_integer(5, type);
34+
auto val6 = from_integer(6, type);
35+
auto val7 = from_integer(7, type);
36+
auto val8 = from_integer(8, type);
37+
auto val9 = from_integer(9, type);
38+
auto val10 = from_integer(10, type);
39+
auto val11 = from_integer(11, type);
40+
auto val12 = from_integer(12, type);
41+
auto interval_5_10 = constant_interval_exprt(val5, val10);
42+
auto interval_1_10 = constant_interval_exprt(val1, val10);
4343

4444
auto config = vsd_configt::constant_domain();
4545
config.context_tracking.data_dependency_context = false;
@@ -169,9 +169,6 @@ SCENARIO(
169169

170170
GIVEN("compact values to create new intervals")
171171
{
172-
const exprt interval_1_4 = constant_interval_exprt(val1, val4);
173-
const exprt interval_9_12 = constant_interval_exprt(val9, val12);
174-
175172
WHEN("compacting { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 }")
176173
{
177174
auto value_set = make_value_set(
@@ -191,9 +188,41 @@ SCENARIO(
191188
ns);
192189
THEN("{ [1, 4], 5, 6, 7, 8, [9, 12] }")
193190
{
191+
auto interval_1_4 = constant_interval_exprt(val1, val4);
192+
auto interval_9_12 = constant_interval_exprt(val9, val12);
193+
194194
EXPECT(
195195
value_set, {val5, val6, val7, val8, interval_1_4, interval_9_12});
196196
}
197197
}
198+
199+
WHEN(
200+
"compacting { -100, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 100 } - pathalogical "
201+
"case with outliers")
202+
{
203+
auto val100minus = from_integer(-100, type);
204+
auto val100 = from_integer(100, type);
205+
auto value_set = make_value_set(
206+
{val100minus,
207+
val2,
208+
val3,
209+
val4,
210+
val5,
211+
val6,
212+
val7,
213+
val8,
214+
val9,
215+
val10,
216+
val11,
217+
val100},
218+
environment,
219+
ns);
220+
THEN("{ [-100, 0], [0, 100] }")
221+
{
222+
auto interval_100minus_0 = constant_interval_exprt(val100minus, val0);
223+
auto interval_0_100 = constant_interval_exprt(val0, val100);
224+
EXPECT(value_set, {interval_100minus_0, interval_0_100});
225+
}
226+
}
198227
}
199-
}
228+
}

0 commit comments

Comments
 (0)