Add simplify_expr step to duplicate_per_byte

The function `duplicate_per_byte` contains a more efficient implementation
when `init_expr` is a constant.
However this feature is never used as the shadow memory module almost
always wraps `init_expr` with a typecast to the type of the shadow
memory.

This commit applies a simplification step in `duplicate_per_byte`,
calling `simplify_expr`, so that the casts may be removed and the more
efficient implementation will be used.

Author: Enrico Steffinlongo

src/util/expr_initializer.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "config.h"
 #include "magic.h"
 #include "namespace.h" // IWYU pragma: keep
+#include "simplify_expr.h"
 #include "std_code.h"
 #include "symbol_table.h"
 
@@ -68,7 +69,7 @@ optionalt<exprt> expr_initializert::expr_initializer_rec(
     else if(init_expr.is_zero())
       result = from_integer(0, type);
     else
-      result = duplicate_per_byte(init_expr, type);
+      result = duplicate_per_byte(init_expr, type, ns);
 
     result.add_source_location()=source_location;
     return result;
@@ -82,7 +83,7 @@ optionalt<exprt> expr_initializert::expr_initializer_rec(
     else if(init_expr.is_zero())
       result = constant_exprt(ID_0, type);
     else
-      result = duplicate_per_byte(init_expr, type);
+      result = duplicate_per_byte(init_expr, type, ns);
 
     result.add_source_location()=source_location;
     return result;
@@ -101,7 +102,7 @@ optionalt<exprt> expr_initializert::expr_initializer_rec(
       result = constant_exprt(value, type);
     }
     else
-      result = duplicate_per_byte(init_expr, type);
+      result = duplicate_per_byte(init_expr, type, ns);
 
     result.add_source_location()=source_location;
     return result;
@@ -121,7 +122,7 @@ optionalt<exprt> expr_initializert::expr_initializer_rec(
       result = complex_exprt(*sub_zero, *sub_zero, to_complex_type(type));
     }
     else
-      result = duplicate_per_byte(init_expr, type);
+      result = duplicate_per_byte(init_expr, type, ns);
 
     result.add_source_location()=source_location;
     return result;
@@ -289,7 +290,7 @@ optionalt<exprt> expr_initializert::expr_initializer_rec(
     else if(init_expr.is_zero())
       result = constant_exprt(irep_idt(), type);
     else
-      result = duplicate_per_byte(init_expr, type);
+      result = duplicate_per_byte(init_expr, type, ns);
 
     result.add_source_location()=source_location;
     return result;
@@ -373,10 +374,14 @@ static exprt cast_or_reinterpret(const exprt &expr, const typet &out_type)
 /// output type.
 /// \param init_byte_expr The initialization expression
 /// \param output_type The output type
+/// \param ns Namespace to perform type symbol/tag lookups
 /// \return The built expression
 /// \note `init_byte_expr` must be a boolean or a bitvector and must be of at
 ///  most `size <= config.ansi_c.char_width`
-exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
+exprt duplicate_per_byte(
+  const exprt &init_byte_expr,
+  const typet &output_type,
+  const namespacet &ns)
 {
   const auto init_type_as_bitvector =
     type_try_dynamic_cast<bitvector_typet>(init_byte_expr.type());
@@ -385,20 +390,25 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
     (init_type_as_bitvector &&
      init_type_as_bitvector->get_width() <= config.ansi_c.char_width) ||
     init_byte_expr.type().id() == ID_bool);
+  // Simplify init_expr to enable faster duplication when simplifiable to a
+  // constant expr
+  const auto simplified_init_expr = simplify_expr(init_byte_expr, ns);
   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
+    // Replicate `simplified_init_expr` enough times until it completely fills
     // `output_type`.
 
     // We've got a constant. So, precompute the value of the constant.
-    if(init_byte_expr.is_constant())
+    if(simplified_init_expr.is_constant())
     {
       const auto init_size = init_type_as_bitvector->get_width();
-      const irep_idt init_value = to_constant_expr(init_byte_expr).get_value();
+      const irep_idt init_value =
+        to_constant_expr(simplified_init_expr).get_value();
 
       // Create a new BV of `output_type` size with its representation being the
-      // replication of the init_byte_expr (padded with 0) enough times to fill.
+      // replication of the simplified_init_expr (padded with 0) enough times to
+      // fill.
       const auto output_value =
         make_bvrep(out_width, [&init_size, &init_value](std::size_t index) {
           // Index modded by 8 to access the i-th bit of init_value
@@ -427,7 +437,7 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
     {
       operation_type = unsignedbv_typet{float_type->get_width()};
     }
-    // Let's cast init_byte_expr to output_type.
+    // Let's cast simplified_init_expr to output_type.
     const exprt casted_init_byte_expr =
       typecast_exprt::conditional_cast(init_byte_expr, operation_type);
     values.push_back(casted_init_byte_expr);

src/util/expr_initializer.h

@@ -33,6 +33,9 @@ optionalt<exprt> expr_initializer(
   const namespacet &ns,
   const exprt &init_byte_expr);
 
-exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type);
+exprt duplicate_per_byte(
+  const exprt &init_byte_expr,
+  const typet &output_type,
+  const namespacet &ns);
 
 #endif // CPROVER_UTIL_EXPR_INITIALIZER_H

unit/util/expr_initializer.cpp

@@ -113,7 +113,8 @@ TEST_CASE(
     const cbmc_invariants_should_throwt invariants_throw;
 
     REQUIRE_THROWS_MATCHES(
-      duplicate_per_byte(array_of_exprt{true_exprt{}, array_type}, input_type),
+      duplicate_per_byte(
+        array_of_exprt{true_exprt{}, array_type}, input_type, test.ns),
       invariant_failedt,
       invariant_failure_containing(
         "Condition: (init_type_as_bitvector && "
@@ -128,7 +129,8 @@ TEST_CASE(
     const cbmc_invariants_should_throwt invariants_throw;
 
     REQUIRE_THROWS_MATCHES(
-      duplicate_per_byte(from_integer(0, unsignedbv_typet{10}), input_type),
+      duplicate_per_byte(
+        from_integer(0, unsignedbv_typet{10}), input_type, test.ns),
       invariant_failedt,
       invariant_failure_containing(
         "init_type_as_bitvector->get_width() <= config.ansi_c.char_width"));
@@ -170,15 +172,17 @@ TEST_CASE(
       typet output_type = unsignedbv_typet{output_size};
       const auto result = duplicate_per_byte(
         from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
-        output_type);
+        output_type,
+        test.ns);
       const auto expected =
         from_integer(output_expected_value, unsignedbv_typet{output_size});
       REQUIRE(result == expected);
 
       // Check that signed-bv values are replicated including the sign bit.
       const auto result_with_signed_init_type = duplicate_per_byte(
         from_integer(init_expr_value, signedbv_typet{init_expr_size}),
-        output_type);
+        output_type,
+        test.ns);
       REQUIRE(result_with_signed_init_type == result);
     }
 
@@ -187,15 +191,17 @@ TEST_CASE(
       typet output_type = signedbv_typet{output_size};
       const auto result = duplicate_per_byte(
         from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
-        output_type);
+        output_type,
+        test.ns);
       const auto expected =
         from_integer(output_expected_value, signedbv_typet{output_size});
       REQUIRE(result == expected);
 
       // Check that signed-bv values are replicated including the sign bit.
       const auto result_with_signed_init_type = duplicate_per_byte(
         from_integer(init_expr_value, signedbv_typet{init_expr_size}),
-        output_type);
+        output_type,
+        test.ns);
       REQUIRE(result_with_signed_init_type == result);
     }
 
@@ -205,7 +211,8 @@ TEST_CASE(
       const pointer_typet output_type{bool_typet{}, output_size};
       const auto result = duplicate_per_byte(
         from_integer(init_expr_value, signedbv_typet{init_expr_size}),
-        output_type);
+        output_type,
+        test.ns);
       auto expected =
         from_integer(output_expected_value, unsignedbv_typet{output_size});
       // Forcing the type to be pointer_typet otherwise from_integer fails when
@@ -219,11 +226,13 @@ TEST_CASE(
       // Check that replicating to a float_value is same as unsigned_bv.
       const auto result = duplicate_per_byte(
         from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
-        float_type());
+        float_type(),
+        test.ns);
       const auto expected_unsigned_value =
         expr_try_dynamic_cast<constant_exprt>(duplicate_per_byte(
           from_integer(init_expr_value, unsignedbv_typet{init_expr_size}),
-          unsignedbv_typet{float_type().get_width()}));
+          unsignedbv_typet{float_type().get_width()},
+          test.ns));
       REQUIRE(expected_unsigned_value);
       const auto expected =
         constant_exprt{expected_unsigned_value->get_value(), float_type()};
@@ -250,13 +259,13 @@ TEST_CASE(
   SECTION("Testing with init size " + std::to_string(init_expr_size))
   {
     const auto init_expr = plus_exprt{
-      from_integer(1, unsignedbv_typet{init_expr_size}),
+      symbol_exprt{"a_symbol", unsignedbv_typet{init_expr_size}},
       from_integer(2, unsignedbv_typet{init_expr_size})};
     SECTION("filling signedbv of size " + std::to_string(output_size))
     {
       typet output_type = signedbv_typet{output_size};
 
-      const auto result = duplicate_per_byte(init_expr, output_type);
+      const auto result = duplicate_per_byte(init_expr, output_type, test.ns);
 
       const auto casted_init_expr =
         typecast_exprt::conditional_cast(init_expr, output_type);
@@ -269,7 +278,7 @@ TEST_CASE(
     SECTION("filling unsignedbv of size " + std::to_string(output_size))
     {
       typet output_type = unsignedbv_typet{output_size};
-      const auto result = duplicate_per_byte(init_expr, output_type);
+      const auto result = duplicate_per_byte(init_expr, output_type, test.ns);
 
       const auto casted_init_expr =
         typecast_exprt::conditional_cast(init_expr, output_type);
@@ -284,7 +293,7 @@ TEST_CASE(
       // Check that replicating a pointer_value is same as unsigned_bv modulo a
       // byte_extract outside.
       const pointer_typet output_type{bool_typet{}, output_size};
-      const auto result = duplicate_per_byte(init_expr, output_type);
+      const auto result = duplicate_per_byte(init_expr, output_type, test.ns);
       const auto unsigned_corr_type = unsignedbv_typet{output_size};
       const auto unsigned_init_expr =
         typecast_exprt::conditional_cast(init_expr, unsigned_corr_type);
@@ -306,7 +315,7 @@ TEST_CASE(
       const std::size_t float_replication_count =
         (float_type().get_width() + config.ansi_c.char_width - 1) /
         config.ansi_c.char_width;
-      const auto result = duplicate_per_byte(init_expr, float_type());
+      const auto result = duplicate_per_byte(init_expr, float_type(), test.ns);
       const auto unsigned_corr_type =
         unsignedbv_typet{float_type().get_width()};
       const auto unsigned_init_expr =
@@ -412,8 +421,8 @@ TEST_CASE(
       const auto result =
         expr_initializer(input_type, test.loc, test.ns, init_value);
       REQUIRE(result.has_value());
-      const auto expected =
-        duplicate_per_byte(init_value, unsignedbv_typet{input_type_size});
+      const auto expected = duplicate_per_byte(
+        init_value, unsignedbv_typet{input_type_size}, test.ns);
       REQUIRE(result.value() == expected);
     }
   }
@@ -460,7 +469,7 @@ TEST_CASE(
         expr_initializer(input_type, test.loc, test.ns, init_value);
       REQUIRE(result.has_value());
       const auto expected = duplicate_per_byte(
-        init_value, pointer_typet{bool_typet{}, input_type_size});
+        init_value, pointer_typet{bool_typet{}, input_type_size}, test.ns);
       REQUIRE(result.value() == expected);
     }
   }
@@ -499,7 +508,8 @@ TEST_CASE("expr_initializer on float type", "[core][util][expr_initializer]")
       const auto result =
         expr_initializer(input_type, test.loc, test.ns, init_value);
       REQUIRE(result.has_value());
-      const auto expected = duplicate_per_byte(init_value, float_type());
+      const auto expected =
+        duplicate_per_byte(init_value, float_type(), test.ns);
       REQUIRE(result.value() == expected);
     }
   }
@@ -562,13 +572,13 @@ TEST_CASE(
       from_integer(0xAB, signedbv_typet{config.ansi_c.char_width});
     const auto result =
       expr_initializer(enum_type, test.loc, test.ns, init_value);
-    const auto expected = duplicate_per_byte(init_value, enum_type);
+    const auto expected = duplicate_per_byte(init_value, enum_type, test.ns);
     REQUIRE(result.has_value());
     REQUIRE(result.value() == expected);
 
     const auto tag_result =
       expr_initializer(c_enum_tag_type, test.loc, test.ns, init_value);
-    auto tag_expected = duplicate_per_byte(init_value, enum_type);
+    auto tag_expected = duplicate_per_byte(init_value, enum_type, test.ns);
     tag_expected.type() = c_enum_tag_type;
     REQUIRE(tag_result.has_value());
     REQUIRE(tag_result.value() == tag_expected);
@@ -624,7 +634,7 @@ TEST_CASE(
       expr_initializer(array_type, test.loc, test.ns, init_value);
     REQUIRE(result.has_value());
     std::vector<exprt> array_values{
-      elem_count, duplicate_per_byte(init_value, inner_type)};
+      elem_count, duplicate_per_byte(init_value, inner_type, test.ns)};
     const auto expected = array_exprt{
       array_values,
       array_typet{
@@ -678,7 +688,7 @@ TEST_CASE(
       expr_initializer(array_type, test.loc, test.ns, init_value);
     REQUIRE(result.has_value());
     const auto expected = array_of_exprt{
-      duplicate_per_byte(init_value, inner_type),
+      duplicate_per_byte(init_value, inner_type, test.ns),
       array_typet{
         inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}};
     REQUIRE(result.value() == expected);
@@ -750,7 +760,7 @@ TEST_CASE(
       expr_initializer(array_type, test.loc, test.ns, init_value);
     REQUIRE(result.has_value());
     std::vector<exprt> inner_array_values{
-      elem_count, duplicate_per_byte(init_value, inner_type)};
+      elem_count, duplicate_per_byte(init_value, inner_type, test.ns)};
     const auto inner_expected = array_exprt{
       inner_array_values,
       array_typet{
@@ -847,12 +857,13 @@ TEST_CASE(
       expr_initializer(struct_type, test.loc, test.ns, init_value);
     REQUIRE(result.has_value());
     const exprt::operandst expected_inner_struct_fields{
-      duplicate_per_byte(init_value, signedbv_typet{32}),
-      duplicate_per_byte(init_value, unsignedbv_typet{16})};
+      duplicate_per_byte(init_value, signedbv_typet{32}, test.ns),
+      duplicate_per_byte(init_value, unsignedbv_typet{16}, test.ns)};
     const struct_exprt expected_inner_struct_expr{
       expected_inner_struct_fields, inner_struct_type};
     const exprt::operandst expected_struct_fields{
-      duplicate_per_byte(init_value, bool_typet{}), expected_inner_struct_expr};
+      duplicate_per_byte(init_value, bool_typet{}, test.ns),
+      expected_inner_struct_expr};
     const struct_exprt expected_struct_expr{
       expected_struct_fields, struct_type};
     REQUIRE(result.value() == expected_struct_expr);
@@ -935,7 +946,9 @@ TEST_CASE("expr_initializer on union type", "[core][util][expr_initializer]")
       expr_initializer(union_type, test.loc, test.ns, init_value);
     REQUIRE(result.has_value());
     const union_exprt expected_union{
-      "foo", duplicate_per_byte(init_value, signedbv_typet{256}), union_type};
+      "foo",
+      duplicate_per_byte(init_value, signedbv_typet{256}, test.ns),
+      union_type};
     REQUIRE(result.value() == expected_union);
 
     const auto union_tag_type =
@@ -945,7 +958,7 @@ TEST_CASE("expr_initializer on union type", "[core][util][expr_initializer]")
     REQUIRE(tag_result.has_value());
     const union_exprt expected_union_tag{
       "foo",
-      duplicate_per_byte(init_value, signedbv_typet{256}),
+      duplicate_per_byte(init_value, signedbv_typet{256}, test.ns),
       union_tag_type};
     REQUIRE(tag_result.value() == expected_union_tag);
   }
@@ -1024,7 +1037,8 @@ TEST_CASE("expr_initializer on string type", "[core][util][expr_initializer]")
     const auto result =
       expr_initializer(string_type, test.loc, test.ns, init_value);
     REQUIRE(result.has_value());
-    const auto expected_string = duplicate_per_byte(init_value, string_type);
+    const auto expected_string =
+      duplicate_per_byte(init_value, string_type, test.ns);
     REQUIRE(result.value() == expected_string);
   }
 }