Skip to content

Commit 5cd42eb

Browse files
jezhigginsjezhiggins
committed
Use widening_range in value_set_abstract_object widening merge
Means widened ranges are calculated in the same way for both intervals and value sets, both now handling max & min appropriately.
1 parent 5efbdcd commit 5cd42eb

File tree

6 files changed

+117
-60
lines changed

6 files changed

+117
-60
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -354,8 +354,8 @@ abstract_object_pointert widening_merge(
354354
auto widened = widened_ranget(lhs, rhs);
355355

356356
// new interval ...
357-
auto new_interval =
358-
constant_interval_exprt(widened.lower_bound, widened.upper_bound);
357+
auto new_interval = constant_interval_exprt(
358+
widened.widened_lower_bound, widened.widened_upper_bound);
359359
return interval_abstract_valuet::make_interval(new_interval);
360360
}
361361

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

Lines changed: 22 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
#include <analyses/variable-sensitivity/context_abstract_object.h>
1515
#include <analyses/variable-sensitivity/interval_abstract_value.h>
1616
#include <analyses/variable-sensitivity/value_set_abstract_object.h>
17+
#include <analyses/variable-sensitivity/widened_range.h>
1718

1819
#include <util/arith_tools.h>
1920
#include <util/make_unique.h>
@@ -414,6 +415,7 @@ static abstract_object_sett compact_values(const abstract_object_sett &values)
414415
}
415416

416417
static exprt eval_expr(const exprt &e);
418+
static bool is_eq(const exprt &lhs, const exprt &rhs);
417419
static bool is_le(const exprt &lhs, const exprt &rhs);
418420
static abstract_object_sett collapse_values_in_intervals(
419421
const abstract_object_sett &values,
@@ -446,6 +448,8 @@ void collapse_overlapping_intervals(
446448
intervals.begin(),
447449
intervals.end(),
448450
[](constant_interval_exprt const &lhs, constant_interval_exprt const &rhs) {
451+
if(is_eq(lhs.get_lower(), rhs.get_lower()))
452+
return is_le(lhs.get_upper(), rhs.get_upper());
449453
return is_le(lhs.get_lower(), rhs.get_lower());
450454
});
451455

@@ -556,10 +560,14 @@ static exprt eval_expr(const exprt &e)
556560
return simplify_expr(e, ns);
557561
}
558562

563+
static bool is_eq(const exprt &lhs, const exprt &rhs)
564+
{
565+
return constant_interval_exprt::equal(lhs, rhs);
566+
}
567+
559568
static bool is_le(const exprt &lhs, const exprt &rhs)
560569
{
561-
auto is_le_expr = binary_relation_exprt(lhs, ID_le, rhs);
562-
return eval_expr(is_le_expr).is_true();
570+
return constant_interval_exprt::less_than_or_equal(lhs, rhs);
563571
}
564572

565573
static abstract_object_sett widen_value_set(
@@ -572,41 +580,34 @@ static abstract_object_sett widen_value_set(
572580

573581
auto widened_ends = std::vector<constant_interval_exprt>{};
574582

575-
auto lower_bound =
576-
constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower());
577-
auto upper_bound =
578-
constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper());
579-
auto range = plus_exprt(
580-
minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
581-
582-
auto symbol_table = symbol_tablet{};
583-
auto ns = namespacet{symbol_table};
583+
auto range = widened_ranget(lhs, rhs);
584584

585585
// should extend lower bound?
586-
if(rhs.get_lower() < lhs.get_lower())
586+
if(range.is_lower_widened)
587587
{
588-
auto widened_lower_bound = constant_interval_exprt(
589-
simplify_expr(minus_exprt(lower_bound, range), ns), lower_bound);
590-
widened_ends.push_back(widened_lower_bound);
588+
auto extended_lower_bound =
589+
constant_interval_exprt(range.widened_lower_bound, range.lower_bound);
590+
591+
widened_ends.push_back(extended_lower_bound);
591592
for(auto &obj : values)
592593
{
593594
auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
594595
auto as_expr = value->to_interval();
595-
if(is_le(as_expr.get_lower(), lower_bound))
596+
if(is_le(as_expr.get_lower(), range.lower_bound))
596597
widened_ends.push_back(as_expr);
597598
}
598599
}
599600
// should extend upper bound?
600-
if(lhs.get_upper() < rhs.get_upper())
601+
if(range.is_upper_widened)
601602
{
602-
auto widened_upper_bound = constant_interval_exprt(
603-
upper_bound, simplify_expr(plus_exprt(upper_bound, range), ns));
604-
widened_ends.push_back(widened_upper_bound);
603+
auto extended_upper_bound =
604+
constant_interval_exprt(range.upper_bound, range.widened_upper_bound);
605+
widened_ends.push_back(extended_upper_bound);
605606
for(auto &obj : values)
606607
{
607608
auto value = std::dynamic_pointer_cast<const abstract_value_objectt>(obj);
608609
auto as_expr = value->to_interval();
609-
if(is_le(upper_bound, as_expr.get_upper()))
610+
if(is_le(range.upper_bound, as_expr.get_upper()))
610611
widened_ends.push_back(as_expr);
611612
}
612613
}

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -20,32 +20,32 @@ static bool has_overflowed(const exprt &value)
2020
value, from_integer(0, value.type()));
2121
}
2222

23-
exprt widened_ranget::make_lower_bound() const
23+
exprt widened_ranget::widen_lower_bound() const
2424
{
25-
if(!lower_extended)
26-
return lower_;
25+
if(!is_lower_widened)
26+
return lower_bound;
2727

28-
auto new_lower_bound = simplify_expr(minus_exprt(lower_, range_), ns_);
28+
auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range_), ns_);
2929

3030
if(
3131
constant_interval_exprt::contains_extreme(new_lower_bound) ||
3232
has_underflowed(new_lower_bound))
33-
return min_exprt(lower_.type());
33+
return min_exprt(lower_bound.type());
3434

3535
return new_lower_bound;
3636
}
3737

38-
exprt widened_ranget::make_upper_bound() const
38+
exprt widened_ranget::widen_upper_bound() const
3939
{
40-
if(!upper_extended)
41-
return upper_;
40+
if(!is_upper_widened)
41+
return upper_bound;
4242

43-
auto new_upper_bound = simplify_expr(plus_exprt(upper_, range_), ns_);
43+
auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range_), ns_);
4444

4545
if(
4646
constant_interval_exprt::contains_extreme(new_upper_bound) ||
4747
has_overflowed(new_upper_bound))
48-
return max_exprt(upper_.type());
48+
return max_exprt(upper_bound.type());
4949

5050
return new_upper_bound;
5151
}

‎src/analyses/variable-sensitivity/widened_range.h‎

Lines changed: 18 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -20,38 +20,39 @@ class widened_ranget
2020
widened_ranget(
2121
const constant_interval_exprt &lhs,
2222
const constant_interval_exprt &rhs)
23-
: lower_extended(
23+
: is_lower_widened(
2424
constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())),
25-
upper_extended(
25+
is_upper_widened(
2626
constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())),
27-
ns_(symbol_tablet{}),
28-
lower_(
27+
lower_bound(
2928
constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())),
30-
upper_(
29+
upper_bound(
3130
constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())),
32-
range_(
33-
plus_exprt(minus_exprt(upper_, lower_), from_integer(1, lhs.type()))),
34-
lower_bound(make_lower_bound()),
35-
upper_bound(make_upper_bound())
31+
ns_(symbol_tablet{}),
32+
range_(plus_exprt(
33+
minus_exprt(upper_bound, lower_bound),
34+
from_integer(1, lhs.type()))),
35+
widened_lower_bound(widen_lower_bound()),
36+
widened_upper_bound(widen_upper_bound())
3637
{
3738
}
3839

39-
const bool lower_extended;
40-
const bool upper_extended;
40+
const bool is_lower_widened;
41+
const bool is_upper_widened;
42+
const exprt lower_bound;
43+
const exprt upper_bound;
4144

4245
private:
4346
namespacet ns_;
44-
exprt lower_;
45-
exprt upper_;
4647
exprt range_;
4748

4849
public:
49-
const exprt lower_bound;
50-
const exprt upper_bound;
50+
const exprt widened_lower_bound;
51+
const exprt widened_upper_bound;
5152

5253
private:
53-
exprt make_lower_bound() const;
54-
exprt make_upper_bound() const;
54+
exprt widen_lower_bound() const;
55+
exprt widen_upper_bound() const;
5556
};
5657

5758
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H

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

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,8 @@ SCENARIO(
4444
const exprt val10minus = from_integer(-10, type);
4545
auto valMax = max_exprt(type);
4646
auto valMin = min_exprt(type);
47+
auto veryLarge = from_integer(2 << 29, type);
48+
auto veryLargeMinus = from_integer(-(2 << 29), type);
4749

4850
auto config = vsd_configt::constant_domain();
4951
config.context_tracking.data_dependency_context = false;
@@ -320,7 +322,6 @@ SCENARIO(
320322
}
321323
WHEN("merging [0, 1] with [1, very_large]")
322324
{
323-
auto veryLarge = from_integer(2 << 29, type);
324325
auto op1 = make_interval(val0, val1, environment, ns);
325326
auto op2 = make_interval(val1, veryLarge, environment, ns);
326327

@@ -346,7 +347,6 @@ SCENARIO(
346347
}
347348
WHEN("merging [0, 1] with [-very_large, 1]")
348349
{
349-
auto veryLargeMinus = from_integer(-(2 << 29), type);
350350
auto op1 = make_interval(val0, val1, environment, ns);
351351
auto op2 = make_interval(veryLargeMinus, val1, environment, ns);
352352

@@ -384,8 +384,6 @@ SCENARIO(
384384
}
385385
WHEN("merging [0, very_large] with [-very_large, 0]")
386386
{
387-
auto veryLarge = from_integer(2 << 29, type);
388-
auto veryLargeMinus = from_integer(-(2 << 29), type);
389387
auto op1 = make_interval(val0, veryLarge, environment, ns);
390388
auto op2 = make_interval(veryLargeMinus, val0, environment, ns);
391389

@@ -398,8 +396,6 @@ SCENARIO(
398396
}
399397
WHEN("merging [-very_large, 0] with [0, very_large]")
400398
{
401-
auto veryLarge = from_integer(2 << 29, type);
402-
auto veryLargeMinus = from_integer(-(2 << 29), type);
403399
auto op1 = make_interval(veryLargeMinus, val0, environment, ns);
404400
auto op2 = make_interval(val0, veryLarge, environment, ns);
405401

@@ -413,8 +409,6 @@ SCENARIO(
413409

414410
WHEN("merging [-very_large, very_large] with [0, 1]")
415411
{
416-
auto veryLarge = from_integer(2 << 29, type);
417-
auto veryLargeMinus = from_integer(-(2 << 29), type);
418412
auto op1 = make_interval(veryLargeMinus, veryLarge, environment, ns);
419413
auto op2 = make_interval(val0, val1, environment, ns);
420414

@@ -427,8 +421,6 @@ SCENARIO(
427421
}
428422
WHEN("merging [0, 1] with [-very_large, very_large]")
429423
{
430-
auto veryLarge = from_integer(2 << 29, type);
431-
auto veryLargeMinus = from_integer(-(2 << 29), type);
432424
auto op1 = make_interval(val0, val1, environment, ns);
433425
auto op2 = make_interval(veryLargeMinus, veryLarge, environment, ns);
434426

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

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,10 @@ SCENARIO(
4747
auto val5minus = from_integer(-5, type);
4848
auto val8minus = from_integer(-8, type);
4949
auto val10minus = from_integer(-10, type);
50+
auto valMax = max_exprt(type);
51+
auto valMin = min_exprt(type);
52+
auto veryLarge = from_integer(2 << 29, type);
53+
auto veryLargeMinus = from_integer(-(2 << 29), type);
5054

5155
auto config = vsd_configt::constant_domain();
5256
config.context_tracking.data_dependency_context = false;
@@ -382,5 +386,64 @@ SCENARIO(
382386
val2minus});
383387
}
384388
}
389+
390+
WHEN("merging {0, very_large} with {-very_large, 0}")
391+
{
392+
auto op1 = make_value_set({val0, veryLarge}, environment, ns);
393+
auto op2 = make_value_set({veryLargeMinus, val0}, environment, ns);
394+
395+
auto merged = widening_merge(op1, op2);
396+
397+
THEN("result is {[MIN, -very_large], 0, very_large]")
398+
{
399+
EXPECT_MODIFIED(
400+
merged,
401+
{constant_interval_exprt(valMin, veryLargeMinus), val0, veryLarge});
402+
}
403+
}
404+
WHEN("merging {-very_large, 0} with {0, very_large}")
405+
{
406+
auto op1 = make_value_set({veryLargeMinus, val0}, environment, ns);
407+
auto op2 = make_value_set({val0, veryLarge}, environment, ns);
408+
409+
auto merged = widening_merge(op1, op2);
410+
411+
THEN("result is {-very_large, 0, [very_large, MAX]}")
412+
{
413+
EXPECT_MODIFIED(
414+
merged,
415+
{veryLargeMinus, val0, constant_interval_exprt(veryLarge, valMax)});
416+
}
417+
}
418+
419+
WHEN("merging {-very_large, very_large } with {0, 1}")
420+
{
421+
auto op1 = make_value_set({veryLargeMinus, veryLarge}, environment, ns);
422+
auto op2 = make_value_set({val0, val1}, environment, ns);
423+
424+
auto merged = widening_merge(op1, op2);
425+
426+
THEN("result is {-very_large, val0, val1, very_large}")
427+
{
428+
EXPECT_MODIFIED(merged, {veryLargeMinus, val0, val1, veryLarge});
429+
}
430+
}
431+
WHEN("merging {0, 1} with {-very_large, very_large}")
432+
{
433+
auto op1 = make_value_set({val0, val1}, environment, ns);
434+
auto op2 = make_value_set({veryLargeMinus, veryLarge}, environment, ns);
435+
436+
auto merged = widening_merge(op1, op2);
437+
438+
THEN("result is {[MIN, 0}, [1, MAX]}")
439+
{
440+
EXPECT_MODIFIED(
441+
merged,
442+
{constant_interval_exprt(valMin, veryLargeMinus),
443+
val0,
444+
val1,
445+
constant_interval_exprt(veryLarge, valMax)});
446+
}
447+
}
385448
}
386449
}

0 commit comments

Comments
 (0)