simplify extractbits_exprt representation

The current representation of extractbits_exprt stores both the upper and
lower indices of the range that is to be extracted, and their difference
plus one in form of the width of the type of the expression.

This removes the upper index, as it can be deduced from the lower index and
the width of the result.  The key benefit is reducing burden on the user of
the class, who a) doesn't have to remember which index comes first, and b)
doesn't have to do the calculation of the upper index.

Author: kroening

src/ansi-c/expr2c.cpp

@@ -3494,9 +3494,18 @@ expr2ct::convert_extractbits(const extractbits_exprt &src, unsigned precedence)
 {
   std::string dest = convert_with_precedence(src.src(), precedence);
   dest+='[';
-  dest += convert_with_precedence(src.upper(), precedence);
+  auto expr_width_opt = pointer_offset_bits(src.type(), ns);
+  if(expr_width_opt.has_value())
+  {
+    auto upper = plus_exprt{
+      src.index(),
+      from_integer(expr_width_opt.value() - 1, src.index().type())};
+    dest += convert_with_precedence(upper, precedence);
+  }
+  else
+    dest += "?";
   dest+=", ";
-  dest += convert_with_precedence(src.lower(), precedence);
+  dest += convert_with_precedence(src.index(), precedence);
   dest+=']';
 
   return dest;

src/ansi-c/goto_check_c.cpp

@@ -973,7 +973,6 @@ void goto_check_ct::integer_overflow_check(
 
       const exprt top_bits = extractbits_exprt(
         op_ext_shifted,
-        new_type.get_width() - 1,
         new_type.get_width() - number_of_top_bits,
         unsignedbv_typet(number_of_top_bits));
 

src/cpp/expr2cpp.cpp

@@ -33,7 +33,6 @@ class expr2cppt:public expr2ct
   std::string convert_cpp_this();
   std::string convert_cpp_new(const exprt &src);
   std::string convert_extractbit(const exprt &src);
-  std::string convert_extractbits(const exprt &src);
   std::string convert_code_cpp_delete(const exprt &src, unsigned indent);
   std::string convert_code_cpp_new(const exprt &src, unsigned indent);
   std::string convert_struct(const exprt &src, unsigned &precedence) override;
@@ -433,11 +432,6 @@ std::string expr2cppt::convert_with_precedence(
     precedence = 15;
     return convert_extractbit(src);
   }
-  else if(src.id()==ID_extractbits)
-  {
-    precedence = 15;
-    return convert_extractbits(src);
-  }
   else if(src.id()==ID_side_effect &&
           (src.get(ID_statement)==ID_cpp_new ||
            src.get(ID_statement)==ID_cpp_new_array))
@@ -489,14 +483,6 @@ std::string expr2cppt::convert_extractbit(const exprt &src)
          "]";
 }
 
-std::string expr2cppt::convert_extractbits(const exprt &src)
-{
-  const auto &extractbits_expr = to_extractbits_expr(src);
-  return convert(extractbits_expr.src()) + ".range(" +
-         convert(extractbits_expr.upper()) + "," +
-         convert(extractbits_expr.lower()) + ")";
-}
-
 std::string expr2cpp(const exprt &expr, const namespacet &ns)
 {
   expr2cppt expr2cpp(ns);

src/solvers/flattening/boolbv_extractbits.cpp

@@ -17,43 +17,28 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
 
   auto const &src_bv = convert_bv(expr.src());
 
-  auto const maybe_upper_as_int = numeric_cast<mp_integer>(expr.upper());
-  auto const maybe_lower_as_int = numeric_cast<mp_integer>(expr.lower());
+  auto const maybe_index_as_int = numeric_cast<mp_integer>(expr.index());
 
   // We only do constants for now.
   // Should implement a shift here.
-  if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value())
+  if(!maybe_index_as_int.has_value())
     return conversion_failed(expr);
 
-  auto upper_as_int = maybe_upper_as_int.value();
-  auto lower_as_int = maybe_lower_as_int.value();
+  auto index_as_int = maybe_index_as_int.value();
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    upper_as_int >= 0 && upper_as_int < src_bv.size(),
-    "upper end of extracted bits must be within the bitvector",
+    index_as_int >= 0 && index_as_int < src_bv.size(),
+    "index of extractbits must be within the bitvector",
     expr.find_source_location(),
     irep_pretty_diagnosticst{expr});
 
   DATA_INVARIANT_WITH_DIAGNOSTICS(
-    lower_as_int >= 0 && lower_as_int < src_bv.size(),
-    "lower end of extracted bits must be within the bitvector",
+    index_as_int + bv_width - 1 < src_bv.size(),
+    "index+width-1 of extractbits must be within the bitvector",
     expr.find_source_location(),
     irep_pretty_diagnosticst{expr});
 
-  DATA_INVARIANT(
-    lower_as_int <= upper_as_int,
-    "upper bound must be greater or equal to lower bound");
-
-  // now lower_as_int <= upper_as_int
-
-  DATA_INVARIANT_WITH_DIAGNOSTICS(
-    (upper_as_int - lower_as_int + 1) == bv_width,
-    "the difference between upper and lower end of the range must have the "
-    "same width as the resulting bitvector type",
-    expr.find_source_location(),
-    irep_pretty_diagnosticst{expr});
-
-  const std::size_t offset = numeric_cast_v<std::size_t>(lower_as_int);
+  const std::size_t offset = numeric_cast_v<std::size_t>(index_as_int);
 
   bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width);
 

src/solvers/floatbv/float_bv.cpp

@@ -92,8 +92,7 @@ exprt float_bvt::convert(const exprt &expr) const
       return nil_exprt{};
     }
 
-    return extractbits_exprt{
-      to_typecast_expr(expr).op(), dest_type.get_width() - 1, 0, dest_type};
+    return extractbits_exprt{to_typecast_expr(expr).op(), 0, dest_type};
   }
   else if(expr.id()==ID_floatbv_plus)
   {
@@ -669,12 +668,11 @@ exprt float_bvt::limit_distance(
     return dist;
 
   const extractbits_exprt upper_bits(
-    dist, dist_width - 1, nb_bits, unsignedbv_typet(dist_width - nb_bits));
+    dist, nb_bits, unsignedbv_typet(dist_width - nb_bits));
   const equal_exprt upper_bits_zero(
     upper_bits, from_integer(0, upper_bits.type()));
 
-  const extractbits_exprt lower_bits(
-    dist, nb_bits - 1, 0, unsignedbv_typet(nb_bits));
+  const extractbits_exprt lower_bits(dist, 0, unsignedbv_typet(nb_bits));
 
   return if_exprt(
     upper_bits_zero,
@@ -924,19 +922,15 @@ exprt float_bvt::get_exponent(
   const exprt &src,
   const ieee_float_spect &spec)
 {
-  return extractbits_exprt(
-    src, spec.f+spec.e-1, spec.f,
-    unsignedbv_typet(spec.e));
+  return extractbits_exprt(src, spec.f, unsignedbv_typet(spec.e));
 }
 
 /// Gets the fraction without hidden bit in a floating-point bit-vector src
 exprt float_bvt::get_fraction(
   const exprt &src,
   const ieee_float_spect &spec)
 {
-  return extractbits_exprt(
-    src, spec.f-1, 0,
-    unsignedbv_typet(spec.f));
+  return extractbits_exprt(src, 0, unsignedbv_typet(spec.f));
 }
 
 exprt float_bvt::isnan(
@@ -975,10 +969,7 @@ void float_bvt::normalization_shift(
 
     // check if first 'distance'-many bits are zeros
     const extractbits_exprt prefix(
-      fraction,
-      fraction_bits - 1,
-      fraction_bits - distance,
-      unsignedbv_typet(distance));
+      fraction, fraction_bits - distance, unsignedbv_typet(distance));
     const equal_exprt prefix_is_zero(prefix, from_integer(0, prefix.type()));
 
     // If so, shift the zeros out left by 'distance'.
@@ -1147,7 +1138,7 @@ exprt float_bvt::fraction_rounding_decision(
     // We keep most-significant bits, and thus the tail is made
     // of least-significant bits.
     const extractbits_exprt tail(
-      fraction, extra_bits - 2, 0, unsignedbv_typet(extra_bits - 2 + 1));
+      fraction, 0, unsignedbv_typet(extra_bits - 2 + 1));
     sticky_bit=notequal_exprt(tail, from_integer(0, tail.type()));
   }
 
@@ -1216,9 +1207,8 @@ void float_bvt::round_fraction(
       fraction_size, result.sign, result.fraction, rounding_mode_bits);
 
     // chop off all the extra bits
-    result.fraction=extractbits_exprt(
-      result.fraction, result_fraction_size-1, extra_bits,
-      unsignedbv_typet(fraction_size));
+    result.fraction = extractbits_exprt(
+      result.fraction, extra_bits, unsignedbv_typet(fraction_size));
 
 #if 0
     // *** does not catch when the overflow goes subnormal -> normal ***
@@ -1306,8 +1296,8 @@ void float_bvt::round_exponent(
   else // exponent gets smaller -- chop off top bits
   {
     exprt old_exponent=result.exponent;
-    result.exponent=
-      extractbits_exprt(result.exponent, spec.e-1, 0, signedbv_typet(spec.e));
+    result.exponent =
+      extractbits_exprt(result.exponent, 0, signedbv_typet(spec.e));
 
     // max_exponent is the maximum representable
     // i.e. 1 higher than the maximum possible for a normal number
@@ -1374,10 +1364,8 @@ float_bvt::biased_floatt float_bvt::bias(
   const extractbit_exprt hidden_bit(src.fraction, spec.f);
   const not_exprt denormal(hidden_bit);
 
-  result.fraction=
-    extractbits_exprt(
-      src.fraction, spec.f-1, 0,
-      unsignedbv_typet(spec.f));
+  result.fraction =
+    extractbits_exprt(src.fraction, 0, unsignedbv_typet(spec.f));
 
   // make exponent zero if its denormal
   // (includes zero)
@@ -1490,7 +1478,7 @@ exprt float_bvt::sticky_right_shift(
     exprt lost_bits;
 
     if(d<=width)
-      lost_bits=extractbits_exprt(result, d-1, 0, unsignedbv_typet(d));
+      lost_bits = extractbits_exprt(result, 0, unsignedbv_typet(d));
     else
       lost_bits=result;
 

src/solvers/smt2/smt2_conv.cpp

@@ -1831,22 +1831,14 @@ void smt2_convt::convert_expr(const exprt &expr)
   else if(expr.id()==ID_extractbits)
   {
     const extractbits_exprt &extractbits_expr = to_extractbits_expr(expr);
+    auto width = boolbv_width(expr.type());
 
-    if(
-      extractbits_expr.upper().is_constant() &&
-      extractbits_expr.lower().is_constant())
+    if(extractbits_expr.index().is_constant())
     {
-      mp_integer op1_i =
-        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.upper()));
-      mp_integer op2_i =
-        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.lower()));
-
-      if(op2_i>op1_i)
-        std::swap(op1_i, op2_i);
-
-      // now op1_i>=op2_i
+      mp_integer index_i =
+        numeric_cast_v<mp_integer>(to_constant_expr(extractbits_expr.index()));
 
-      out << "((_ extract " << op1_i << " " << op2_i << ") ";
+      out << "((_ extract " << (width + index_i - 1) << " " << index_i << ") ";
       flatten2bv(extractbits_expr.src());
       out << ")";
     }

src/solvers/smt2/smt2_parser.cpp

@@ -638,15 +638,14 @@ exprt smt2_parsert::function_application()
           if(op.size()!=1)
             throw error("extract takes one operand");
 
-          auto upper_e=from_integer(upper, integer_typet());
-          auto lower_e=from_integer(lower, integer_typet());
-
           if(upper<lower)
             throw error("extract got bad indices");
 
+          auto lower_e = from_integer(lower, integer_typet());
+
           unsignedbv_typet t(upper-lower+1);
 
-          return extractbits_exprt(op[0], upper_e, lower_e, t);
+          return extractbits_exprt(op[0], lower_e, t);
         }
         else if(id=="rotate_left" ||
                 id=="rotate_right" ||

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1111,10 +1111,14 @@ static smt_termt convert_expr_to_smt(
   const sub_expression_mapt &converted)
 {
   const smt_termt &from = converted.at(extract_bits.src());
-  const auto upper_value = numeric_cast<std::size_t>(extract_bits.upper());
-  const auto lower_value = numeric_cast<std::size_t>(extract_bits.lower());
-  if(upper_value && lower_value)
-    return smt_bit_vector_theoryt::extract(*upper_value, *lower_value)(from);
+  const auto bit_vector_sort =
+    convert_type_to_smt_sort(extract_bits.type()).cast<smt_bit_vector_sortt>();
+  INVARIANT(
+    bit_vector_sort, "Extract can only be applied to bit vector terms.");
+  const auto index_value = numeric_cast<std::size_t>(extract_bits.index());
+  if(index_value)
+    return smt_bit_vector_theoryt::extract(
+      *index_value + bit_vector_sort->bit_width() - 1, *index_value)(from);
   UNIMPLEMENTED_FEATURE(
     "Generation of SMT formula for extract bits expression: " +
     extract_bits.pretty());

src/solvers/smt2_incremental/encoding/struct_encoding.cpp

@@ -195,7 +195,6 @@ static std::size_t count_trailing_bit_width(
 exprt struct_encodingt::encode_member(const member_exprt &member_expr) const
 {
   const auto &type = ns.get().follow(member_expr.compound().type());
-  const auto member_bits_width = (*boolbv_width)(member_expr.type());
   const auto offset_bits = [&]() -> std::size_t {
     if(can_cast_type<union_typet>(type))
       return 0;
@@ -204,10 +203,7 @@ exprt struct_encodingt::encode_member(const member_exprt &member_expr) const
       struct_type, member_expr.get_component_name(), *boolbv_width);
   }();
   return extractbits_exprt{
-    member_expr.compound(),
-    offset_bits + member_bits_width - 1,
-    offset_bits,
-    member_expr.type()};
+    member_expr.compound(), offset_bits, member_expr.type()};
 }
 
 exprt struct_encodingt::encode(exprt expr) const

src/solvers/strings/string_constraint_generator_float.cpp

@@ -28,8 +28,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 ///   in octuple precision.
 exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
 {
-  const extractbits_exprt exp_bits(
-    src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e));
+  const extractbits_exprt exp_bits(src, spec.f, unsignedbv_typet(spec.e));
 
   // Exponent is in biased form (numbers from -128 to 127 are encoded with
   // integer from 0 to 255) we have to remove the bias.
@@ -44,7 +43,7 @@ exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
 /// \return An unsigned value representing the fractional part.
 exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
 {
-  return extractbits_exprt(src, spec.f - 1, 0, unsignedbv_typet(spec.f));
+  return extractbits_exprt(src, 0, unsignedbv_typet(spec.f));
 }
 
 /// Gets the significand as a java integer, looking for the hidden bit.