introduce update_bits_exprt

This introduces update_bits_exprt, which allows replacing parts of a
bit-vector identified by a (potentially variable) index by a given
bit-vector.

This supersedes with_exprt in the case of single-bit operands.

src/solvers/Makefile

@@ -128,6 +128,7 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/boolbv_unary_minus.cpp \
       flattening/boolbv_union.cpp \
       flattening/boolbv_update.cpp \
+      flattening/boolbv_update_bits.cpp \
       flattening/boolbv_width.cpp \
       flattening/boolbv_with.cpp \
       flattening/bv_dimacs.cpp \

src/solvers/flattening/boolbv.h

@@ -39,6 +39,7 @@ class overflow_result_exprt;
 class replication_exprt;
 class unary_overflow_exprt;
 class union_typet;
+class update_bits_exprt;
 
 class boolbvt:public arrayst
 {
@@ -176,6 +177,7 @@ class boolbvt:public arrayst
   virtual bvt convert_member(const member_exprt &expr);
   virtual bvt convert_with(const with_exprt &expr);
   virtual bvt convert_update(const update_exprt &);
+  virtual bvt convert_update_bits(const update_bits_exprt &);
   virtual bvt convert_case(const exprt &expr);
   virtual bvt convert_cond(const cond_exprt &);
   virtual bvt convert_shift(const binary_exprt &expr);
@@ -196,6 +198,8 @@ class boolbvt:public arrayst
   virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
   virtual bvt convert_overflow_result(const overflow_result_exprt &expr);
 
+  bvt convert_update_bits(bvt src, const exprt &index, const bvt &new_value);
+
   void convert_with(
     const typet &type,
     const exprt &where,

src/solvers/flattening/boolbv_update_bits.cpp

@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <util/bitvector_expr.h>
+
+#include "boolbv.h"
+
+bvt boolbvt::convert_update_bits(const update_bits_exprt &expr)
+{
+  return convert_bv(expr.lower());
+}

src/solvers/smt2/smt2_conv.cpp

@@ -1683,6 +1683,10 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     convert_update(to_update_expr(expr));
   }
+  else if(expr.id() == ID_update_bits)
+  {
+    convert_update_bits(to_update_bits_expr(expr));
+  }
   else if(expr.id() == ID_object_address)
   {
     out << "(object-address ";
@@ -4338,6 +4342,11 @@ void smt2_convt::convert_update(const update_exprt &expr)
   SMT2_TODO("smt2_convt::convert_update to be implemented");
 }
 
+void smt2_convt::convert_update_bits(const update_bits_exprt &expr)
+{
+  return convert_expr(expr.lower());
+}
+
 void smt2_convt::convert_index(const index_exprt &expr)
 {
   const typet &array_op_type = expr.array().type();

src/solvers/smt2/smt2_conv.h

@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H
 #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H
 
+#include <util/bitvector_expr.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/threeval.h>
@@ -149,6 +150,7 @@ class smt2_convt : public stack_decision_proceduret
 
   void convert_with(const with_exprt &expr);
   void convert_update(const update_exprt &);
+  void convert_update_bits(const update_bits_exprt &);
 
   void convert_expr(const exprt &);
   void convert_type(const typet &);

src/util/bitvector_expr.cpp

@@ -42,6 +42,36 @@ extractbits_exprt::extractbits_exprt(
     from_integer(_lower, integer_typet()));
 }
 
+exprt update_bits_exprt::lower() const
+{
+  const auto width = to_bitvector_type(type()).get_width();
+  const auto new_value_width =
+    to_bitvector_type(new_value().type()).get_width();
+  auto src_bv_type = bv_typet(width);
+
+  // build a mask 1...1 0...0
+  auto mask_bv = make_bvrep(width, [new_value_width](std::size_t index) {
+    return index >= new_value_width;
+  });
+  auto mask_expr = constant_exprt(mask_bv, src_bv_type);
+
+  // shift the mask by the index
+  auto mask_shifted = shl_exprt(mask_expr, index());
+
+  auto src_masked =
+    bitand_exprt(typecast_exprt(src(), src_bv_type), mask_shifted);
+
+  // zero-extend or shrink the replacement bits to match src
+  auto new_value_casted = typecast_exprt(new_value(), src_bv_type);
+
+  // shift the replacement bits
+  auto new_value_shifted = shl_exprt(new_value_casted, index());
+
+  // or the masked src and the shifted replacement bits
+  return typecast_exprt(
+    bitor_exprt(src_masked, new_value_shifted), src().type());
+}
+
 exprt popcount_exprt::lower() const
 {
   // Hacker's Delight, variant pop0:

src/util/bitvector_expr.h

@@ -531,6 +531,92 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
   return ret;
 }
 
+/// \brief Replaces a sub-range of a bit-vector operand
+class update_bits_exprt : public expr_protectedt
+{
+public:
+  /// Replace the bits [\p _index .. \p _index + size] from \p _src
+  /// where size is the width of \p _new_value to produce a result of
+  /// the same type as \p _src. The index counts from the
+  /// least-significant bit.
+  update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
+    : expr_protectedt(
+        ID_update_bits,
+        _src.type(),
+        {_src, std::move(_index), std::move(_new_value)})
+  {
+  }
+
+  update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value);
+
+  exprt &src()
+  {
+    return op0();
+  }
+
+  exprt &index()
+  {
+    return op1();
+  }
+
+  exprt &new_value()
+  {
+    return op2();
+  }
+
+  const exprt &src() const
+  {
+    return op0();
+  }
+
+  const exprt &index() const
+  {
+    return op1();
+  }
+
+  const exprt &new_value() const
+  {
+    return op2();
+  }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    validate_operands(expr, 3, "update_bits must have three operands");
+  }
+
+  /// A lowering to masking, shifting, or.
+  exprt lower() const;
+};
+
+template <>
+inline bool can_cast_expr<update_bits_exprt>(const exprt &base)
+{
+  return base.id() == ID_update_bits;
+}
+
+/// \brief Cast an exprt to an \ref update_bits_exprt
+///
+/// \a expr must be known to be \ref update_bits_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref update_bits_exprt
+inline const update_bits_exprt &to_update_bits_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_update_bits);
+  update_bits_exprt::check(expr);
+  return static_cast<const update_bits_exprt &>(expr);
+}
+
+/// \copydoc to_update_bits_expr(const exprt &)
+inline update_bits_exprt &to_update_bits_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_update_bits);
+  update_bits_exprt::check(expr);
+  return static_cast<update_bits_exprt &>(expr);
+}
+
 /// \brief Bit-vector replication
 class replication_exprt : public binary_exprt
 {

src/util/irep_ids.def

@@ -185,6 +185,7 @@ IREP_ID_ONE(exists)
 IREP_ID_ONE(repeat)
 IREP_ID_ONE(extractbit)
 IREP_ID_ONE(extractbits)
+IREP_ID_ONE(update_bits)
 IREP_ID_TWO(C_reference, #reference)
 IREP_ID_TWO(C_rvalue_reference, #rvalue_reference)
 IREP_ID_ONE(true)