Unit test lower_byte_extract to/from an array of bits

Byte operator lowering made several assumptions about array elements
being byte aligned, which may be true for ANSI C, but isn't the case for
our C front-end (which supports arrays of single bits), and not true for
the overall framework in general.

Author: tautschnig

unit/solvers/lowering/byte_operators.cpp

@@ -24,6 +24,88 @@
 #include <util/string_constant.h>
 #include <util/symbol_table.h>
 
+TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
+{
+  // this test does require a proper architecture to be set so that byte extract
+  // uses adequate endianness
+  cmdlinet cmdline;
+  config.set(cmdline);
+
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  const unsignedbv_typet u16{16};
+  const exprt sixteen_bits = from_integer(0x1234, u16);
+  const array_typet bit_array_type{bv_typet{1}, from_integer(16, size_type())};
+
+  bool little_endian;
+  GIVEN("Little endian")
+  {
+    little_endian = true;
+
+    const auto bit_string = expr2bits(sixteen_bits, little_endian, ns);
+    REQUIRE(bit_string.has_value());
+    REQUIRE(bit_string->size() == 16);
+
+    const auto array_of_bits =
+      bits2expr(*bit_string, bit_array_type, little_endian, ns);
+    REQUIRE(array_of_bits.has_value());
+
+    const auto bit_string2 = expr2bits(*array_of_bits, little_endian, ns);
+    REQUIRE(bit_string2.has_value());
+    REQUIRE(*bit_string == *bit_string2);
+
+    const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian
+                                               : ID_byte_extract_big_endian,
+                                 sixteen_bits,
+                                 from_integer(0, index_type()),
+                                 bit_array_type};
+    const exprt lower_be1 = lower_byte_extract(be1, ns);
+    REQUIRE(lower_be1 == *array_of_bits);
+
+    const byte_extract_exprt be2{little_endian ? ID_byte_extract_little_endian
+                                               : ID_byte_extract_big_endian,
+                                 *array_of_bits,
+                                 from_integer(0, index_type()),
+                                 u16};
+    const exprt lower_be2 = lower_byte_extract(be2, ns);
+    REQUIRE(lower_be2 == sixteen_bits);
+  }
+
+  GIVEN("Big endian")
+  {
+    little_endian = false;
+
+    const auto bit_string = expr2bits(sixteen_bits, little_endian, ns);
+    REQUIRE(bit_string.has_value());
+    REQUIRE(bit_string->size() == 16);
+
+    const auto array_of_bits =
+      bits2expr(*bit_string, bit_array_type, little_endian, ns);
+    REQUIRE(array_of_bits.has_value());
+
+    const auto bit_string2 = expr2bits(*array_of_bits, little_endian, ns);
+    REQUIRE(bit_string2.has_value());
+    REQUIRE(*bit_string == *bit_string2);
+
+    const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian
+                                               : ID_byte_extract_big_endian,
+                                 sixteen_bits,
+                                 from_integer(0, index_type()),
+                                 bit_array_type};
+    const exprt lower_be1 = lower_byte_extract(be1, ns);
+    REQUIRE(lower_be1 == *array_of_bits);
+
+    const byte_extract_exprt be2{little_endian ? ID_byte_extract_little_endian
+                                               : ID_byte_extract_big_endian,
+                                 *array_of_bits,
+                                 from_integer(0, index_type()),
+                                 u16};
+    const exprt lower_be2 = lower_byte_extract(be2, ns);
+    REQUIRE(lower_be2 == sixteen_bits);
+  }
+}
+
 SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
 {
   // this test does require a proper architecture to be set so that byte extract
@@ -196,6 +278,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       union_typet({{"compA", u32}, {"compB", u64}}),
       c_enum_typet(u16),
       c_enum_typet(unsignedbv_typet(128)),
+      array_typet{bv_typet{1}, from_integer(128, size_type())},
       array_typet(u8, size),
       array_typet(s32, size),
       array_typet(u64, size),