Merge pull request #7872 from esteffin/esteffin/fix-shadow-memory-float-duplication

Fix shadow memory float issue

Author: NlightNFotis

regression/cbmc-shadow-memory/float1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

src/util/expr_initializer.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "arith_tools.h"
 #include "bitvector_expr.h"
+#include "byte_operators.h"
 #include "c_types.h"
 #include "config.h"
 #include "magic.h"
@@ -344,6 +345,27 @@ optionalt<exprt> expr_initializer(
   return expr_initializert(ns)(type, source_location, init_byte_expr);
 }
 
+/// Typecast the input to the output if this is a signed/unsigned bv.
+/// Perform a reinterpret cast using byte_extract otherwise.
+/// @param expr the expression to be casted if necessary.
+/// @param out_type the type to cast the expression to.
+/// @return the casted or reinterpreted expression.
+static exprt cast_or_reinterpret(const exprt &expr, const typet &out_type)
+{
+  // Same type --> no cast
+  if(expr.type() == out_type)
+  {
+    return expr;
+  }
+  if(
+    can_cast_type<signedbv_typet>(out_type) ||
+    can_cast_type<unsignedbv_typet>(out_type))
+  {
+    return typecast_exprt::conditional_cast(expr, out_type);
+  }
+  return make_byte_extract(expr, from_integer(0, char_type()), out_type);
+}
+
 /// 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.
@@ -375,7 +397,7 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
       const auto init_size = init_type_as_bitvector->get_width();
       const irep_idt init_value = to_constant_expr(init_byte_expr).get_value();
 
-      // Create a new BV od `output_type` size with its representation being the
+      // 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.
       const auto output_value =
         make_bvrep(out_width, [&init_size, &init_value](std::size_t index) {
@@ -400,6 +422,11 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
     {
       operation_type = unsignedbv_typet{ptr_type->get_width()};
     }
+    if(
+      const auto float_type = type_try_dynamic_cast<floatbv_typet>(output_type))
+    {
+      operation_type = unsignedbv_typet{float_type->get_width()};
+    }
     // Let's cast init_byte_expr to output_type.
     const exprt casted_init_byte_expr =
       typecast_exprt::conditional_cast(init_byte_expr, operation_type);
@@ -410,10 +437,10 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type)
         casted_init_byte_expr,
         from_integer(config.ansi_c.char_width * i, size_type())));
     }
-    if(values.size() == 1)
-      return typecast_exprt::conditional_cast(values[0], output_type);
-    return typecast_exprt::conditional_cast(
-      multi_ary_exprt(ID_bitor, values, operation_type), output_type);
+    return cast_or_reinterpret(
+      values.size() == 1 ? values[0]
+                         : multi_ary_exprt(ID_bitor, values, operation_type),
+      output_type);
   }
 
   // Anything else. We don't know what to do with it. So, just cast.

unit/util/expr_initializer.cpp

@@ -3,6 +3,7 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>
@@ -142,7 +143,7 @@ std::string to_hex(unsigned int value)
 }
 
 TEST_CASE(
-  "duplicate_per_byte on unsigned_bv with constant",
+  "duplicate_per_byte on bitvector types with constant",
   "[core][util][duplicate_per_byte]")
 {
   auto test = expr_initializer_test_environmentt::make();
@@ -161,34 +162,73 @@ TEST_CASE(
       rowt{0xAB, 8, 0xABAB, 16},   // smaller-type constant gets replicated
       rowt{0xAB, 8, 0xBABAB, 20}); // smaller-type constant gets replicated
   SECTION(
-    "Testing with output size " + std::to_string(output_size) + " init value " +
-    to_hex(init_expr_value) + " of size " + std::to_string(init_expr_size))
+    "Testing with init value " + to_hex(init_expr_value) + " of size " +
+    std::to_string(init_expr_size))
   {
-    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);
-    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);
-    REQUIRE(result_with_signed_init_type == result);
-
-    // Check that replicating a pointer_value is same as unsigned_bv.
-    const pointer_typet pointer_type{bool_typet{}, output_size};
-    const auto result_with_pointer_type = duplicate_per_byte(
-      from_integer(init_expr_value, signedbv_typet{init_expr_size}),
-      pointer_type);
-    auto pointer_typed_expected =
-      from_integer(output_expected_value, unsignedbv_typet{output_size});
-    // Forcing the type to be pointer_typet otherwise from_integer fails when
-    // the init value is not 0 (NULL).
-    pointer_typed_expected.type() = pointer_type;
-    REQUIRE(result_with_pointer_type == pointer_typed_expected);
+    SECTION("filling unsignedbv of size " + std::to_string(output_size))
+    {
+      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);
+      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);
+      REQUIRE(result_with_signed_init_type == result);
+    }
+
+    SECTION("filling signedbv of size " + std::to_string(output_size))
+    {
+      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);
+      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);
+      REQUIRE(result_with_signed_init_type == result);
+    }
+
+    SECTION("filling pointer of size " + std::to_string(output_size))
+    {
+      // Check that replicating a pointer_value is same as unsigned_bv.
+      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);
+      auto expected =
+        from_integer(output_expected_value, unsignedbv_typet{output_size});
+      // Forcing the type to be pointer_typet otherwise from_integer fails when
+      // the init value is not 0 (NULL).
+      expected.type() = output_type;
+      REQUIRE(result == expected);
+    }
+
+    SECTION("filling float")
+    {
+      // 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());
+      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()}));
+      REQUIRE(expected_unsigned_value);
+      const auto expected =
+        constant_exprt{expected_unsigned_value->get_value(), float_type()};
+      REQUIRE(result == expected);
+    }
   }
 }
 
@@ -207,38 +247,78 @@ TEST_CASE(
     rowt{8, 2, 1},   // bigger type gets truncated
     rowt{8, 16, 2},  // replicated twice
     rowt{8, 20, 3}); // replicated three times and truncated
-  SECTION(
-    "Testing with output size " + std::to_string(output_size) + " init size " +
-    std::to_string(init_expr_size))
+  SECTION("Testing with init size " + std::to_string(init_expr_size))
   {
-    typet output_type = signedbv_typet{output_size};
-
     const auto init_expr = plus_exprt{
       from_integer(1, unsignedbv_typet{init_expr_size}),
       from_integer(2, unsignedbv_typet{init_expr_size})};
-    const auto result = duplicate_per_byte(init_expr, output_type);
+    SECTION("filling signedbv of size " + std::to_string(output_size))
+    {
+      typet output_type = signedbv_typet{output_size};
 
-    const auto casted_init_expr =
-      typecast_exprt::conditional_cast(init_expr, output_type);
-    const auto expected =
-      replicate_expression(casted_init_expr, output_type, replication_count);
+      const auto result = duplicate_per_byte(init_expr, output_type);
 
-    REQUIRE(result == expected);
+      const auto casted_init_expr =
+        typecast_exprt::conditional_cast(init_expr, output_type);
+      const auto expected =
+        replicate_expression(casted_init_expr, output_type, replication_count);
+
+      REQUIRE(result == expected);
+    }
 
-    // Check that replicating a pointer_value is same as unsigned_bv modulo a
-    // typecast outside.
-    const pointer_typet pointer_type{bool_typet{}, output_size};
-    const auto pointer_typed_result =
-      duplicate_per_byte(init_expr, pointer_type);
-    const auto pointer_unsigned_corr_type = unsignedbv_typet{output_size};
-    const auto pointer_init_expr =
-      typecast_exprt::conditional_cast(init_expr, pointer_unsigned_corr_type);
-    const auto pointer_expected = typecast_exprt::conditional_cast(
-      replicate_expression(
-        pointer_init_expr, pointer_unsigned_corr_type, replication_count),
-      pointer_type);
+    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);
 
-    REQUIRE(pointer_typed_result == pointer_expected);
+      const auto casted_init_expr =
+        typecast_exprt::conditional_cast(init_expr, output_type);
+      const auto expected =
+        replicate_expression(casted_init_expr, output_type, replication_count);
+
+      REQUIRE(result == expected);
+    }
+
+    SECTION("filling pointer of size " + std::to_string(output_size))
+    {
+      // 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 unsigned_corr_type = unsignedbv_typet{output_size};
+      const auto unsigned_init_expr =
+        typecast_exprt::conditional_cast(init_expr, unsigned_corr_type);
+      const auto expected = make_byte_extract(
+        replicate_expression(
+          unsigned_init_expr, unsigned_corr_type, replication_count),
+        from_integer(0, char_type()),
+        output_type);
+
+      REQUIRE(result == expected);
+    }
+
+    SECTION("filling float")
+    {
+      // Check that replicating a float is same as unsigned_bv modulo a
+      // byte_extract outside.
+      // We ignore the output size and replication_count passed above as float
+      // size is constant
+      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 unsigned_corr_type =
+        unsignedbv_typet{float_type().get_width()};
+      const auto unsigned_init_expr =
+        typecast_exprt::conditional_cast(init_expr, unsigned_corr_type);
+      const auto expected = make_byte_extract(
+        replicate_expression(
+          unsigned_init_expr, unsigned_corr_type, float_replication_count),
+        from_integer(0, char_type()),
+        float_type());
+
+      REQUIRE(result == expected);
+    }
   }
 }
 
@@ -386,6 +466,45 @@ TEST_CASE(
   }
 }
 
+TEST_CASE("expr_initializer on float type", "[core][util][expr_initializer]")
+{
+  auto test = expr_initializer_test_environmentt::make();
+  SECTION("Testing with expected type as float")
+  {
+    const typet input_type = float_type();
+    SECTION("nondet_initializer works")
+    {
+      const auto result = nondet_initializer(input_type, test.loc, test.ns);
+      REQUIRE(result.has_value());
+      const auto expected = side_effect_expr_nondett{float_type(), test.loc};
+      REQUIRE(result.value() == expected);
+      const auto expr_result =
+        expr_initializer(input_type, test.loc, test.ns, exprt(ID_nondet));
+      REQUIRE(expr_result == result);
+    }
+    SECTION("zero_initializer works")
+    {
+      const auto result = zero_initializer(input_type, test.loc, test.ns);
+      REQUIRE(result.has_value());
+      auto expected = from_integer(0, float_type());
+      REQUIRE(result.value() == expected);
+      const auto expr_result = expr_initializer(
+        input_type, test.loc, test.ns, constant_exprt(ID_0, char_type()));
+      REQUIRE(expr_result == result);
+    }
+    SECTION("expr_initializer calls duplicate_per_byte")
+    {
+      const exprt init_value =
+        from_integer(0x0A, unsignedbv_typet{config.ansi_c.char_width});
+      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());
+      REQUIRE(result.value() == expected);
+    }
+  }
+}
+
 TEST_CASE(
   "expr_initializer on c_enum and c_enum_tag",
   "[core][util][expr_initializer]")