Skip to content

Commit bf32f63

Browse files
tautschnigtautschnig
authored
Merge pull request #7931 from tautschnig/cleanup/min-max-value
Rename {min,max}_exprt to {min,max}_value_exprt
2 parents 3ce2140 + 7243b70 commit bf32f63

File tree

22 files changed

+149
-109
lines changed

22 files changed

+149
-109
lines changed

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -787,7 +787,7 @@ exprt assume_less_than_unbounded(
787787
{
788788
// TOP < x, so prune range is min->right.upper
789789
auto pruned_expr = constant_interval_exprt(
790-
min_exprt(operands.left->type()),
790+
min_value_exprt(operands.left->type()),
791791
operands.right_interval().get_upper(),
792792
operands.left->type());
793793
auto constrained =
@@ -799,7 +799,7 @@ exprt assume_less_than_unbounded(
799799
// x < TOP, so prune range is left.lower->max
800800
auto pruned_expr = constant_interval_exprt(
801801
operands.left_interval().get_lower(),
802-
max_exprt(operands.right->type()),
802+
max_value_exprt(operands.right->type()),
803803
operands.right->type());
804804
auto constrained =
805805
std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);

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

Lines changed: 13 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -106,13 +106,13 @@ bvint_value_is_min(const typet &type, const mp_integer &value)
106106
static inline constant_interval_exprt
107107
interval_from_x_le_value(const exprt &value)
108108
{
109-
return constant_interval_exprt(min_exprt(value.type()), value);
109+
return constant_interval_exprt(min_value_exprt(value.type()), value);
110110
}
111111

112112
static inline constant_interval_exprt
113113
interval_from_x_ge_value(const exprt &value)
114114
{
115-
return constant_interval_exprt(value, max_exprt(value.type()));
115+
return constant_interval_exprt(value, max_value_exprt(value.type()));
116116
}
117117

118118
static inline mp_integer force_value_from_expr(const exprt &value)
@@ -129,7 +129,8 @@ interval_from_x_lt_value(const exprt &value)
129129
mp_integer integer_value = force_value_from_expr(value);
130130
if(!bvint_value_is_min(value.type(), integer_value))
131131
return constant_interval_exprt(
132-
min_exprt(value.type()), from_integer(integer_value - 1, value.type()));
132+
min_value_exprt(value.type()),
133+
from_integer(integer_value - 1, value.type()));
133134
else
134135
return constant_interval_exprt::bottom(value.type());
135136
}
@@ -140,7 +141,8 @@ interval_from_x_gt_value(const exprt &value)
140141
mp_integer integer_value = force_value_from_expr(value);
141142
if(!bvint_value_is_max(value.type(), integer_value))
142143
return constant_interval_exprt(
143-
from_integer(integer_value + 1, value.type()), max_exprt(value.type()));
144+
from_integer(integer_value + 1, value.type()),
145+
max_value_exprt(value.type()));
144146
else
145147
return constant_interval_exprt::bottom(value.type());
146148
}
@@ -322,7 +324,7 @@ void interval_abstract_valuet::output(
322324
std::string lower_string;
323325
std::string upper_string;
324326

325-
if(interval.get_lower().id() == ID_min)
327+
if(interval.get_lower().id() == ID_min_value)
326328
{
327329
lower_string = "-INF";
328330
}
@@ -334,7 +336,7 @@ void interval_abstract_valuet::output(
334336
id2string(to_constant_expr(interval.get_lower()).get_value());
335337
}
336338

337-
if(interval.get_upper().id() == ID_max)
339+
if(interval.get_upper().id() == ID_max_value)
338340
{
339341
upper_string = "+INF";
340342
}
@@ -420,8 +422,12 @@ interval_abstract_valuet::index_range_implementation(const namespacet &ns) const
420422
{
421423
if(is_top() || is_bottom() || interval.is_top() || interval.is_bottom())
422424
return make_empty_index_range();
423-
if(interval.get_lower().id() == ID_min || interval.get_upper().id() == ID_max)
425+
if(
426+
interval.get_lower().id() == ID_min_value ||
427+
interval.get_upper().id() == ID_max_value)
428+
{
424429
return make_empty_index_range();
430+
}
425431

426432
return make_interval_index_range(interval, ns);
427433
}

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -442,11 +442,11 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
442442
set,
443443
[](const abstract_value_objectt &value) {
444444
auto c = value.to_constant();
445-
return c.is_false() || (c.id() == ID_min);
445+
return c.is_false() || (c.id() == ID_min_value);
446446
},
447447
[](const abstract_value_objectt &value) {
448448
auto c = value.to_constant();
449-
return c.is_true() || (c.id() == ID_max);
449+
return c.is_true() || (c.id() == ID_max_value);
450450
});
451451
}
452452

@@ -456,11 +456,11 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
456456
set,
457457
[](const abstract_value_objectt &value) {
458458
auto c = value.to_constant();
459-
return c.is_zero() || (c.id() == ID_min);
459+
return c.is_zero() || (c.id() == ID_min_value);
460460
},
461461
[](const abstract_value_objectt &value) {
462462
auto c = value.to_constant();
463-
return c.is_one() || (c.id() == ID_max);
463+
return c.is_one() || (c.id() == ID_max_value);
464464
});
465465
}
466466

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ exprt widened_ranget::widen_lower_bound() const
2929
if(
3030
constant_interval_exprt::contains_extreme(new_lower_bound) ||
3131
has_underflowed(new_lower_bound))
32-
return min_exprt(lower_bound.type());
32+
return min_value_exprt(lower_bound.type());
3333

3434
return new_lower_bound;
3535
}
@@ -44,7 +44,7 @@ exprt widened_ranget::widen_upper_bound() const
4444
if(
4545
constant_interval_exprt::contains_extreme(new_upper_bound) ||
4646
has_overflowed(new_upper_bound, upper_bound))
47-
return max_exprt(upper_bound.type());
47+
return max_value_exprt(upper_bound.type());
4848

4949
return new_upper_bound;
5050
}

‎src/util/interval.cpp

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ constant_interval_exprt::plus(const constant_interval_exprt &o) const
8383

8484
if(is_max(get_upper()) || is_max(o.get_upper()))
8585
{
86-
upper = max_exprt(type());
86+
upper = max_value_exprt(type());
8787
}
8888
else
8989
{
@@ -95,7 +95,7 @@ constant_interval_exprt::plus(const constant_interval_exprt &o) const
9595

9696
if(is_min(get_lower()) || is_min(o.get_lower()))
9797
{
98-
lower = min_exprt(type());
98+
lower = min_value_exprt(type());
9999
}
100100
else
101101
{
@@ -559,11 +559,11 @@ exprt constant_interval_exprt::get_extreme(
559559
/* Return top */
560560
if(min_value)
561561
{
562-
return min_exprt(type);
562+
return min_value_exprt(type);
563563
}
564564
else
565565
{
566-
return max_exprt(type);
566+
return max_value_exprt(type);
567567
}
568568

569569
UNREACHABLE;
@@ -651,8 +651,8 @@ void constant_interval_exprt::append_multiply_expression_max(
651651
collection.push_back(expr);
652652
else
653653
{
654-
collection.push_back(max_exprt(expr));
655-
collection.push_back(min_exprt(expr));
654+
collection.push_back(max_value_exprt(expr));
655+
collection.push_back(min_value_exprt(expr));
656656
}
657657
}
658658

@@ -676,8 +676,8 @@ void constant_interval_exprt::append_multiply_expression_min(
676676
collection.push_back(other);
677677
else
678678
{
679-
collection.push_back(min_exprt(min));
680-
collection.push_back(max_exprt(min));
679+
collection.push_back(min_value_exprt(min));
680+
collection.push_back(max_value_exprt(min));
681681
}
682682
}
683683

@@ -698,7 +698,7 @@ exprt constant_interval_exprt::generate_division_expression(
698698
{
699699
if(is_negative(rhs))
700700
{
701-
return min_exprt(lhs);
701+
return min_value_exprt(lhs);
702702
}
703703

704704
return lhs;
@@ -708,7 +708,7 @@ exprt constant_interval_exprt::generate_division_expression(
708708
{
709709
if(is_negative(rhs))
710710
{
711-
return max_exprt(lhs);
711+
return max_value_exprt(lhs);
712712
}
713713

714714
return lhs;
@@ -753,7 +753,7 @@ exprt constant_interval_exprt::generate_modulo_expression(
753753
{
754754
if(is_negative(rhs))
755755
{
756-
return min_exprt(lhs);
756+
return min_value_exprt(lhs);
757757
}
758758

759759
return lhs;
@@ -763,7 +763,7 @@ exprt constant_interval_exprt::generate_modulo_expression(
763763
{
764764
if(is_negative(rhs))
765765
{
766-
return max_exprt(lhs);
766+
return max_value_exprt(lhs);
767767
}
768768

769769
return lhs;
@@ -924,7 +924,7 @@ exprt constant_interval_exprt::generate_shift_expression(
924924

925925
if(is_max(rhs))
926926
{
927-
return min_exprt(rhs);
927+
return min_value_exprt(rhs);
928928
}
929929

930930
INVARIANT(
@@ -1019,14 +1019,14 @@ constant_exprt constant_interval_exprt::zero() const
10191019
return zero(type());
10201020
}
10211021

1022-
min_exprt constant_interval_exprt::min() const
1022+
min_value_exprt constant_interval_exprt::min() const
10231023
{
1024-
return min_exprt(type());
1024+
return min_value_exprt(type());
10251025
}
10261026

1027-
max_exprt constant_interval_exprt::max() const
1027+
max_value_exprt constant_interval_exprt::max() const
10281028
{
1029-
return max_exprt(type());
1029+
return max_value_exprt(type());
10301030
}
10311031

10321032
bool constant_interval_exprt::is_top() const
@@ -1047,7 +1047,7 @@ constant_interval_exprt constant_interval_exprt::top(const typet &type)
10471047

10481048
constant_interval_exprt constant_interval_exprt::bottom(const typet &type)
10491049
{
1050-
return constant_interval_exprt(max_exprt(type), min_exprt(type));
1050+
return constant_interval_exprt(max_value_exprt(type), min_value_exprt(type));
10511051
}
10521052

10531053
constant_interval_exprt constant_interval_exprt::top() const
@@ -1215,12 +1215,12 @@ bool constant_interval_exprt::has_no_lower_bound() const
12151215

12161216
bool constant_interval_exprt::is_max(const exprt &expr)
12171217
{
1218-
return expr.id() == ID_max;
1218+
return expr.id() == ID_max_value;
12191219
}
12201220

12211221
bool constant_interval_exprt::is_min(const exprt &expr)
12221222
{
1223-
return expr.id() == ID_min;
1223+
return expr.id() == ID_min_value;
12241224
}
12251225

12261226
bool constant_interval_exprt::is_positive(const exprt &expr)
@@ -1301,7 +1301,7 @@ exprt constant_interval_exprt::abs(const exprt &expr)
13011301
{
13021302
if(is_signed(expr) && is_min(expr))
13031303
{
1304-
return max_exprt(expr);
1304+
return max_value_exprt(expr);
13051305
}
13061306

13071307
if(is_max(expr) || is_unsigned(expr) || is_zero(expr) || is_positive(expr))
@@ -1641,7 +1641,7 @@ constant_interval_exprt::typecast(const typet &type) const
16411641
else
16421642
{
16431643
auto do_typecast = [&type](exprt e) {
1644-
if(e.id() == ID_min || e.id() == ID_max)
1644+
if(e.id() == ID_min_value || e.id() == ID_max_value)
16451645
{
16461646
e.type() = type;
16471647
}

‎src/util/interval.h

Lines changed: 19 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -14,35 +14,39 @@
1414
#include <iosfwd>
1515

1616
/// +∞ upper bound for intervals
17-
class max_exprt : public nullary_exprt
17+
class max_value_exprt : public nullary_exprt
1818
{
1919
public:
20-
explicit max_exprt(const typet &_type) : nullary_exprt(ID_max, _type)
20+
explicit max_value_exprt(const typet &_type)
21+
: nullary_exprt(ID_max_value, _type)
2122
{
2223
}
2324

24-
explicit max_exprt(const exprt &_expr) : nullary_exprt(ID_max, _expr.type())
25+
explicit max_value_exprt(const exprt &_expr)
26+
: nullary_exprt(ID_max_value, _expr.type())
2527
{
2628
}
2729
};
2830

2931
/// -∞ upper bound for intervals
30-
class min_exprt : public nullary_exprt
32+
class min_value_exprt : public nullary_exprt
3133
{
3234
public:
33-
explicit min_exprt(const typet &_type) : nullary_exprt(ID_min, _type)
35+
explicit min_value_exprt(const typet &_type)
36+
: nullary_exprt(ID_min_value, _type)
3437
{
3538
}
3639

37-
explicit min_exprt(const exprt &_expr) : nullary_exprt(ID_min, _expr.type())
40+
explicit min_value_exprt(const exprt &_expr)
41+
: nullary_exprt(ID_min_value, _expr.type())
3842
{
3943
}
4044
};
4145

4246
/// Represents an interval of values.
4347
/// Bounds should be constant expressions
44-
/// or min_exprt for the lower bound
45-
/// or max_exprt for the upper bound
48+
/// or min_value_exprt for the lower bound
49+
/// or max_value_exprt for the upper bound
4650
/// Also, lower bound should always be <= upper bound
4751
class constant_interval_exprt : public binary_exprt
4852
{
@@ -58,7 +62,10 @@ class constant_interval_exprt : public binary_exprt
5862
}
5963

6064
explicit constant_interval_exprt(const typet &type)
61-
: constant_interval_exprt(min_exprt(type), max_exprt(type), type)
65+
: constant_interval_exprt(
66+
min_value_exprt(type),
67+
max_value_exprt(type),
68+
type)
6269
{
6370
}
6471

@@ -100,7 +107,7 @@ class constant_interval_exprt : public binary_exprt
100107

101108
bool b = true;
102109

103-
b &= expr.is_constant() || id == ID_min || id == ID_max;
110+
b &= expr.is_constant() || id == ID_min_value || id == ID_max_value;
104111

105112
if(expr.is_boolean() && id == ID_constant)
106113
{
@@ -347,8 +354,8 @@ class constant_interval_exprt : public binary_exprt
347354
static bool is_max(const exprt &expr);
348355

349356
/* Generate min and max exprt according to current type */
350-
min_exprt min() const;
351-
max_exprt max() const;
357+
min_value_exprt min() const;
358+
max_value_exprt max() const;
352359

353360
constant_exprt zero() const;
354361
static constant_exprt zero(const typet &type);

‎src/util/irep_ids.def

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -856,8 +856,8 @@ IREP_ID_ONE(statement_list_jump_conditional)
856856
IREP_ID_ONE(statement_list_jump_conditional_not)
857857
IREP_ID_ONE(statement_list_instruction)
858858
IREP_ID_ONE(statement_list_instructions)
859-
IREP_ID_ONE(max)
860-
IREP_ID_ONE(min)
859+
IREP_ID_ONE(max_value)
860+
IREP_ID_ONE(min_value)
861861
IREP_ID_ONE(constant_interval)
862862
IREP_ID_TWO(C_bounds_check, #bounds_check)
863863
IREP_ID_ONE(count_leading_zeros)

‎unit/analyses/variable-sensitivity/interval_abstract_value/extremes-go-top.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@
2222
static void
2323
verify_extreme_interval(typet type, abstract_environmentt &env, namespacet &ns)
2424
{
25-
auto interval = make_interval(min_exprt(type), max_exprt(type), env, ns);
25+
auto interval =
26+
make_interval(min_value_exprt(type), max_value_exprt(type), env, ns);
2627

2728
EXPECT_TOP(interval);
2829
}

0 commit comments

Comments
 (0)