Merge pull request #7931 from tautschnig/cleanup/min-max-value

Rename {min,max}_exprt to {min,max}_value_exprt

Author: tautschnig

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -787,7 +787,7 @@ exprt assume_less_than_unbounded(
   {
     // TOP < x, so prune range is min->right.upper
     auto pruned_expr = constant_interval_exprt(
-      min_exprt(operands.left->type()),
+      min_value_exprt(operands.left->type()),
       operands.right_interval().get_upper(),
       operands.left->type());
     auto constrained =
@@ -799,7 +799,7 @@ exprt assume_less_than_unbounded(
     // x < TOP, so prune range is left.lower->max
     auto pruned_expr = constant_interval_exprt(
       operands.left_interval().get_lower(),
-      max_exprt(operands.right->type()),
+      max_value_exprt(operands.right->type()),
       operands.right->type());
     auto constrained =
       std::make_shared<interval_abstract_valuet>(pruned_expr, env, ns);

src/analyses/variable-sensitivity/interval_abstract_value.cpp

@@ -106,13 +106,13 @@ bvint_value_is_min(const typet &type, const mp_integer &value)
 static inline constant_interval_exprt
 interval_from_x_le_value(const exprt &value)
 {
-  return constant_interval_exprt(min_exprt(value.type()), value);
+  return constant_interval_exprt(min_value_exprt(value.type()), value);
 }
 
 static inline constant_interval_exprt
 interval_from_x_ge_value(const exprt &value)
 {
-  return constant_interval_exprt(value, max_exprt(value.type()));
+  return constant_interval_exprt(value, max_value_exprt(value.type()));
 }
 
 static inline mp_integer force_value_from_expr(const exprt &value)
@@ -129,7 +129,8 @@ interval_from_x_lt_value(const exprt &value)
   mp_integer integer_value = force_value_from_expr(value);
   if(!bvint_value_is_min(value.type(), integer_value))
     return constant_interval_exprt(
-      min_exprt(value.type()), from_integer(integer_value - 1, value.type()));
+      min_value_exprt(value.type()),
+      from_integer(integer_value - 1, value.type()));
   else
     return constant_interval_exprt::bottom(value.type());
 }
@@ -140,7 +141,8 @@ interval_from_x_gt_value(const exprt &value)
   mp_integer integer_value = force_value_from_expr(value);
   if(!bvint_value_is_max(value.type(), integer_value))
     return constant_interval_exprt(
-      from_integer(integer_value + 1, value.type()), max_exprt(value.type()));
+      from_integer(integer_value + 1, value.type()),
+      max_value_exprt(value.type()));
   else
     return constant_interval_exprt::bottom(value.type());
 }
@@ -322,7 +324,7 @@ void interval_abstract_valuet::output(
     std::string lower_string;
     std::string upper_string;
 
-    if(interval.get_lower().id() == ID_min)
+    if(interval.get_lower().id() == ID_min_value)
     {
       lower_string = "-INF";
     }
@@ -334,7 +336,7 @@ void interval_abstract_valuet::output(
         id2string(to_constant_expr(interval.get_lower()).get_value());
     }
 
-    if(interval.get_upper().id() == ID_max)
+    if(interval.get_upper().id() == ID_max_value)
     {
       upper_string = "+INF";
     }
@@ -420,8 +422,12 @@ interval_abstract_valuet::index_range_implementation(const namespacet &ns) const
 {
   if(is_top() || is_bottom() || interval.is_top() || interval.is_bottom())
     return make_empty_index_range();
-  if(interval.get_lower().id() == ID_min || interval.get_upper().id() == ID_max)
+  if(
+    interval.get_lower().id() == ID_min_value ||
+    interval.get_upper().id() == ID_max_value)
+  {
     return make_empty_index_range();
+  }
 
   return make_interval_index_range(interval, ns);
 }

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -442,11 +442,11 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
       set,
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_false() || (c.id() == ID_min);
+        return c.is_false() || (c.id() == ID_min_value);
       },
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_true() || (c.id() == ID_max);
+        return c.is_true() || (c.id() == ID_max_value);
       });
   }
 
@@ -456,11 +456,11 @@ static bool is_set_extreme(const typet &type, const abstract_object_sett &set)
       set,
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_zero() || (c.id() == ID_min);
+        return c.is_zero() || (c.id() == ID_min_value);
       },
       [](const abstract_value_objectt &value) {
         auto c = value.to_constant();
-        return c.is_one() || (c.id() == ID_max);
+        return c.is_one() || (c.id() == ID_max_value);
       });
   }
 

src/analyses/variable-sensitivity/widened_range.cpp

@@ -29,7 +29,7 @@ exprt widened_ranget::widen_lower_bound() const
   if(
     constant_interval_exprt::contains_extreme(new_lower_bound) ||
     has_underflowed(new_lower_bound))
-    return min_exprt(lower_bound.type());
+    return min_value_exprt(lower_bound.type());
 
   return new_lower_bound;
 }
@@ -44,7 +44,7 @@ exprt widened_ranget::widen_upper_bound() const
   if(
     constant_interval_exprt::contains_extreme(new_upper_bound) ||
     has_overflowed(new_upper_bound, upper_bound))
-    return max_exprt(upper_bound.type());
+    return max_value_exprt(upper_bound.type());
 
   return new_upper_bound;
 }

src/util/interval.cpp

@@ -83,7 +83,7 @@ constant_interval_exprt::plus(const constant_interval_exprt &o) const
 
   if(is_max(get_upper()) || is_max(o.get_upper()))
   {
-    upper = max_exprt(type());
+    upper = max_value_exprt(type());
   }
   else
   {
@@ -95,7 +95,7 @@ constant_interval_exprt::plus(const constant_interval_exprt &o) const
 
   if(is_min(get_lower()) || is_min(o.get_lower()))
   {
-    lower = min_exprt(type());
+    lower = min_value_exprt(type());
   }
   else
   {
@@ -559,11 +559,11 @@ exprt constant_interval_exprt::get_extreme(
   /* Return top */
   if(min_value)
   {
-    return min_exprt(type);
+    return min_value_exprt(type);
   }
   else
   {
-    return max_exprt(type);
+    return max_value_exprt(type);
   }
 
   UNREACHABLE;
@@ -651,8 +651,8 @@ void constant_interval_exprt::append_multiply_expression_max(
     collection.push_back(expr);
   else
   {
-    collection.push_back(max_exprt(expr));
-    collection.push_back(min_exprt(expr));
+    collection.push_back(max_value_exprt(expr));
+    collection.push_back(min_value_exprt(expr));
   }
 }
 
@@ -676,8 +676,8 @@ void constant_interval_exprt::append_multiply_expression_min(
     collection.push_back(other);
   else
   {
-    collection.push_back(min_exprt(min));
-    collection.push_back(max_exprt(min));
+    collection.push_back(min_value_exprt(min));
+    collection.push_back(max_value_exprt(min));
   }
 }
 
@@ -698,7 +698,7 @@ exprt constant_interval_exprt::generate_division_expression(
   {
     if(is_negative(rhs))
     {
-      return min_exprt(lhs);
+      return min_value_exprt(lhs);
     }
 
     return lhs;
@@ -708,7 +708,7 @@ exprt constant_interval_exprt::generate_division_expression(
   {
     if(is_negative(rhs))
     {
-      return max_exprt(lhs);
+      return max_value_exprt(lhs);
     }
 
     return lhs;
@@ -753,7 +753,7 @@ exprt constant_interval_exprt::generate_modulo_expression(
   {
     if(is_negative(rhs))
     {
-      return min_exprt(lhs);
+      return min_value_exprt(lhs);
     }
 
     return lhs;
@@ -763,7 +763,7 @@ exprt constant_interval_exprt::generate_modulo_expression(
   {
     if(is_negative(rhs))
     {
-      return max_exprt(lhs);
+      return max_value_exprt(lhs);
     }
 
     return lhs;
@@ -924,7 +924,7 @@ exprt constant_interval_exprt::generate_shift_expression(
 
   if(is_max(rhs))
   {
-    return min_exprt(rhs);
+    return min_value_exprt(rhs);
   }
 
   INVARIANT(
@@ -1019,14 +1019,14 @@ constant_exprt constant_interval_exprt::zero() const
   return zero(type());
 }
 
-min_exprt constant_interval_exprt::min() const
+min_value_exprt constant_interval_exprt::min() const
 {
-  return min_exprt(type());
+  return min_value_exprt(type());
 }
 
-max_exprt constant_interval_exprt::max() const
+max_value_exprt constant_interval_exprt::max() const
 {
-  return max_exprt(type());
+  return max_value_exprt(type());
 }
 
 bool constant_interval_exprt::is_top() const
@@ -1047,7 +1047,7 @@ constant_interval_exprt constant_interval_exprt::top(const typet &type)
 
 constant_interval_exprt constant_interval_exprt::bottom(const typet &type)
 {
-  return constant_interval_exprt(max_exprt(type), min_exprt(type));
+  return constant_interval_exprt(max_value_exprt(type), min_value_exprt(type));
 }
 
 constant_interval_exprt constant_interval_exprt::top() const
@@ -1215,12 +1215,12 @@ bool constant_interval_exprt::has_no_lower_bound() const
 
 bool constant_interval_exprt::is_max(const exprt &expr)
 {
-  return expr.id() == ID_max;
+  return expr.id() == ID_max_value;
 }
 
 bool constant_interval_exprt::is_min(const exprt &expr)
 {
-  return expr.id() == ID_min;
+  return expr.id() == ID_min_value;
 }
 
 bool constant_interval_exprt::is_positive(const exprt &expr)
@@ -1301,7 +1301,7 @@ exprt constant_interval_exprt::abs(const exprt &expr)
 {
   if(is_signed(expr) && is_min(expr))
   {
-    return max_exprt(expr);
+    return max_value_exprt(expr);
   }
 
   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
   else
   {
     auto do_typecast = [&type](exprt e) {
-      if(e.id() == ID_min || e.id() == ID_max)
+      if(e.id() == ID_min_value || e.id() == ID_max_value)
       {
         e.type() = type;
       }

src/util/interval.h

@@ -14,35 +14,39 @@
 #include <iosfwd>
 
 /// +∞ upper bound for intervals
-class max_exprt : public nullary_exprt
+class max_value_exprt : public nullary_exprt
 {
 public:
-  explicit max_exprt(const typet &_type) : nullary_exprt(ID_max, _type)
+  explicit max_value_exprt(const typet &_type)
+    : nullary_exprt(ID_max_value, _type)
   {
   }
 
-  explicit max_exprt(const exprt &_expr) : nullary_exprt(ID_max, _expr.type())
+  explicit max_value_exprt(const exprt &_expr)
+    : nullary_exprt(ID_max_value, _expr.type())
   {
   }
 };
 
 /// -∞ upper bound for intervals
-class min_exprt : public nullary_exprt
+class min_value_exprt : public nullary_exprt
 {
 public:
-  explicit min_exprt(const typet &_type) : nullary_exprt(ID_min, _type)
+  explicit min_value_exprt(const typet &_type)
+    : nullary_exprt(ID_min_value, _type)
   {
   }
 
-  explicit min_exprt(const exprt &_expr) : nullary_exprt(ID_min, _expr.type())
+  explicit min_value_exprt(const exprt &_expr)
+    : nullary_exprt(ID_min_value, _expr.type())
   {
   }
 };
 
 /// Represents an interval of values.
 /// Bounds should be constant expressions
-/// or min_exprt for the lower bound
-/// or max_exprt for the upper bound
+/// or min_value_exprt for the lower bound
+/// or max_value_exprt for the upper bound
 /// Also, lower bound should always be <= upper bound
 class constant_interval_exprt : public binary_exprt
 {
@@ -58,7 +62,10 @@ class constant_interval_exprt : public binary_exprt
   }
 
   explicit constant_interval_exprt(const typet &type)
-    : constant_interval_exprt(min_exprt(type), max_exprt(type), type)
+    : constant_interval_exprt(
+        min_value_exprt(type),
+        max_value_exprt(type),
+        type)
   {
   }
 
@@ -100,7 +107,7 @@ class constant_interval_exprt : public binary_exprt
 
     bool b = true;
 
-    b &= expr.is_constant() || id == ID_min || id == ID_max;
+    b &= expr.is_constant() || id == ID_min_value || id == ID_max_value;
 
     if(expr.is_boolean() && id == ID_constant)
     {
@@ -347,8 +354,8 @@ class constant_interval_exprt : public binary_exprt
   static bool is_max(const exprt &expr);
 
   /* Generate min and max exprt according to current type */
-  min_exprt min() const;
-  max_exprt max() const;
+  min_value_exprt min() const;
+  max_value_exprt max() const;
 
   constant_exprt zero() const;
   static constant_exprt zero(const typet &type);

src/util/irep_ids.def

@@ -856,8 +856,8 @@ IREP_ID_ONE(statement_list_jump_conditional)
 IREP_ID_ONE(statement_list_jump_conditional_not)
 IREP_ID_ONE(statement_list_instruction)
 IREP_ID_ONE(statement_list_instructions)
-IREP_ID_ONE(max)
-IREP_ID_ONE(min)
+IREP_ID_ONE(max_value)
+IREP_ID_ONE(min_value)
 IREP_ID_ONE(constant_interval)
 IREP_ID_TWO(C_bounds_check, #bounds_check)
 IREP_ID_ONE(count_leading_zeros)

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

@@ -22,7 +22,8 @@
 static void
 verify_extreme_interval(typet type, abstract_environmentt &env, namespacet &ns)
 {
-  auto interval = make_interval(min_exprt(type), max_exprt(type), env, ns);
+  auto interval =
+    make_interval(min_value_exprt(type), max_value_exprt(type), env, ns);
 
   EXPECT_TOP(interval);
 }