Merge pull request #8246 from diffblue/extractbits-width

simplify `extractbits_exprt` representation

Author: kroening

src/ansi-c/expr2c.cpp

@@ -3497,9 +3497,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

@@ -999,7 +999,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, [email protected]
 ///   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.