Improved checks and fixed duplicate_per_byte

Author: Enrico Steffinlongo

src/util/expr_initializer.cpp

@@ -346,17 +346,28 @@ optionalt<exprt> expr_initializer(
 /// Builds an expression of the given output type with each of its bytes
 /// initialized to the given initialization expression.
 /// Integer bitvector types are currently supported.
-/// For unsupported types the initialization expression is casted to the
+/// For unsupported `output_type` the initialization expression is casted to the
 /// output type.
 /// \param init_byte_expr The initialization expression
 /// \param output_type The output type
 /// \return The built expression
+/// \note `init_byte_expr` must be of bitvector type and must be of
+///  `size <= config.ansi_c.char_width`
 exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
 {
-  if(output_type.id() == ID_unsignedbv || output_type.id() == ID_signedbv)
+  const auto init_type_as_bitvector =
+    type_try_dynamic_cast<bitvector_typet>(init_byte_expr.type());
+  // Fail if `init_byte_expr` is not a bitvector of maximum 8 bits.
+  PRECONDITION(
+    init_type_as_bitvector &&
+    init_type_as_bitvector->get_width() <= config.ansi_c.char_width);
+  if(const auto output_bv = type_try_dynamic_cast<bitvector_typet>(output_type))
   {
+    const auto out_width = output_bv->get_width();
+    // Replicate `init_byte_expr` enough times until it completely fills
+    // `output_type`.
     const size_t size =
-      to_bitvector_type(output_type).get_width() / config.ansi_c.char_width;
+      (out_width + config.ansi_c.char_width - 1) / config.ansi_c.char_width;
 
     // We've got a constant. So, precompute the value of the constant.
     if(init_byte_expr.is_constant())
@@ -374,11 +385,14 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
 
     // We haven't got a constant. So, build the expression using shift-and-or.
     exprt::operandst values;
-    values.push_back(init_byte_expr);
+    // Let's cast init_byte_expr to output_type.
+    const exprt casted_init_byte_expr =
+      typecast_exprt::conditional_cast(init_byte_expr, output_type);
+    values.push_back(casted_init_byte_expr);
     for(size_t i = 1; i < size; ++i)
     {
       values.push_back(shl_exprt(
-        init_byte_expr,
+        casted_init_byte_expr,
         from_integer(config.ansi_c.char_width * i, size_type())));
     }
     if(values.size() == 1)