Merge pull request #6485 from tautschnig/bv_typet-endianness

bv_typet is also sensitive to endianness

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -50,10 +50,7 @@ static boundst map_bounds(
 
     // big-endian bounds need swapping
     if(result.ub < result.lb)
-    {
-      result.lb = endianness_map.number_of_bits() - result.lb - 1;
-      result.ub = endianness_map.number_of_bits() - result.ub - 1;
-    }
+      std::swap(result.lb, result.ub);
   }
 
   return result;
@@ -1295,7 +1292,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
     concatenation_exprt concatenation(
       std::move(op), bitvector_typet(subtype->id(), width_bytes * 8));
 
-    endianness_mapt map(src.type(), little_endian, ns);
+    endianness_mapt map(concatenation.type(), little_endian, ns);
     return bv_to_expr(concatenation, src.type(), map, ns);
   }
 }
@@ -2226,22 +2223,16 @@ static exprt lower_byte_update(
     // original_bits |= newvalue
     bitor_exprt bitor_expr{bitand_expr, value_shifted};
 
-    if(!is_little_endian && bit_width > type_bits)
-    {
-      return simplify_expr(
-        typecast_exprt::conditional_cast(
-          extractbits_exprt{bitor_expr,
-                            bit_width - 1,
-                            bit_width - type_bits,
-                            bv_typet{type_bits}},
-          src.type()),
-        ns);
-    }
-    else if(bit_width > type_bits)
+    if(bit_width > type_bits)
     {
+      endianness_mapt endianness_map(
+        bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns);
+      const auto bounds = map_bounds(endianness_map, 0, type_bits - 1);
+
       return simplify_expr(
         typecast_exprt::conditional_cast(
-          extractbits_exprt{bitor_expr, type_bits - 1, 0, bv_typet{type_bits}},
+          extractbits_exprt{
+            bitor_expr, bounds.ub, bounds.lb, bv_typet{type_bits}},
           src.type()),
         ns);
     }

src/util/endianness_map.cpp

@@ -53,12 +53,10 @@ void endianness_mapt::build_big_endian(const typet &src)
 {
   if(src.id() == ID_c_enum_tag)
     build_big_endian(ns.follow_tag(to_c_enum_tag_type(src)));
-  else if(src.id()==ID_unsignedbv ||
-          src.id()==ID_signedbv ||
-          src.id()==ID_fixedbv ||
-          src.id()==ID_floatbv ||
-          src.id()==ID_c_enum ||
-          src.id()==ID_c_bit_field)
+  else if(
+    src.id() == ID_unsignedbv || src.id() == ID_signedbv ||
+    src.id() == ID_fixedbv || src.id() == ID_floatbv || src.id() == ID_c_enum ||
+    src.id() == ID_c_bit_field || src.id() == ID_bv)
   {
     // these do get re-ordered!
     auto bits = pointer_offset_bits(src, ns); // error is -1

unit/solvers/lowering/byte_operators.cpp

@@ -24,6 +24,72 @@
 #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);
+  }
+
+  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);
+  }
+}
+
 SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
 {
   // this test does require a proper architecture to be set so that byte extract